1  /-
  2  Copyright (c) 2017 Microsoft Corporation. All rights reserved.
  3  Released under Apache 2.0 license as described in the file LICENSE.
  4  Authors: Leonardo de Moura, Mario Carneiro
  5  -/
  6  import data.list.basic data.pnat.basic data.array.lemmas
src         └─────────────┘ └─────────────┘ └───────────────┘
  7     logic.basic algebra.group
src     └─────────┘ └───────────┘
  8     data.list.defs data.nat.basic data.option.basic
src     └────────────┘ └────────────┘ └───────────────┘
  9     data.bool data.prod
src     └───────┘ └───────┘
 10  import tactic.finish data.sigma.basic
src         └───────────┘ └──────────────┘
 11  
 12  universes u v w
 13  
 14  /-- `bucket_array α β` is the underlying data type for `hash_map α β`,
 15    an array of linked lists of key-value pairs. -/
 16  def bucket_array (α : Type u) (β : α → Type v) (n : ℕ+) :=
id                                                      └┘
src                                                      └┘
typ                                                     └┘
doc                                                      └┘
 17  array n.1 (list Σ a, β a)
id   └───┘    └──┘    
src  └───┘     └──┘   
typ  └───┘    └──┘    
 18  
 19  /-- Make a hash_map index from a `nat` hash value and a (positive) buffer size -/
 20  def hash_map.mk_idx (n : ℕ+) (i : nat) : fin n.1 :=
id                            └┘       └─┘    └─┘ 
src                           └┘       └─┘    └─┘  
typ                           └┘       └─┘    └─┘ 
doc                           └┘
 21  ⟨i % n.1, nat.mod_lt _ n.2⟩
id         └────────┘   
src          └────────┘    
typ        └────────┘   
 22  
 23  namespace bucket_array
 24  section
 25  parameters {α : Type u} {β : α → Type v} (hash_fn : α → nat)
id                                                           └─┘
src                                                          └─┘
typ                                                          └─┘
 26  variables {n : ℕ+} (data : bucket_array α β n)
id                  └┘          └──────────┘
src                 └┘          └──────────┘
typ                 └┘          └──────────┘
doc                 └┘          └──────────┘
 27  
 28  instance : inhabited (bucket_array α β n) :=
id              └───────┘  └──────────┘   
src             └───────┘  └──────────┘
typ             └───────┘  └──────────┘   
doc                        └──────────┘
 29  ⟨mk_array _ []⟩
id    └──────┘   └┘
src   └──────┘   └┘
typ   └──────┘   └┘
 30  
 31  /-- Read the bucket corresponding to an element -/
 32  def read (a : α) : list Σ a, β a :=
id                     └──┘    
src                     └──┘   
typ                    └──┘    
 33  let bidx := hash_map.mk_idx n (hash_fn a) in
id       └──┘    └─────────────┘   └─────┘ 
src              └─────────────┘
typ      └──┘    └─────────────┘   └─────┘ 
doc              └─────────────┘
 34  data.read bidx
id   └──┘└───┘ └──┘
src      └───┘
typ  └──┘└───┘ └──┘
 35  
 36  /-- Write the bucket corresponding to an element -/
 37  def write (a : α) (l : list Σ a, β a) : bucket_array α β n :=
id                         └──┘        └──────────┘   
src                         └──┘           └──────────┘
typ                        └──┘        └──────────┘   
doc                                          └──────────┘
 38  let bidx := hash_map.mk_idx n (hash_fn a) in
id       └──┘    └─────────────┘   └─────┘ 
src              └─────────────┘
typ      └──┘    └─────────────┘   └─────┘ 
doc              └─────────────┘
 39  data.write bidx l
id   └──┘└────┘ └──┘ 
src      └────┘
typ  └──┘└────┘ └──┘ 
 40  
 41  /-- Modify (read, apply `f`, and write) the bucket corresponding to an element -/
 42  def modify (a : α) (f : list (Σ a, β a) → list (Σ a, β a)) : bucket_array α β n :=
id                          └──┘         └──┘          └──────────┘   
src                          └──┘            └──┘             └──────────┘
typ                         └──┘         └──┘          └──────────┘   
doc                                                               └──────────┘
 43  let bidx := hash_map.mk_idx n (hash_fn a) in
id       └──┘    └─────────────┘   └─────┘ 
src              └─────────────┘
typ      └──┘    └─────────────┘   └─────┘ 
doc              └─────────────┘
 44  array.write data bidx (f (array.read data bidx))
id   └─────────┘ └──┘ └──┘    └────────┘ └──┘ └──┘
src  └─────────┘               └────────┘
typ  └─────────┘ └──┘ └──┘    └────────┘ └──┘ └──┘
 45  
 46  /-- The list of all key-value pairs in the bucket list -/
 47  def as_list : list Σ a, β a := data.to_list.join
id                 └──┘        └──┘└──────┘└───┘
src                └──┘               └──────┘└───┘
typ                └──┘        └──┘└──────┘└───┘
 48  
 49  theorem mem_as_list {a : Σ a, β a} : a ∈ data.as_list ↔ ∃i, a ∈ array.read data i :=
id                                     └──┘└──────┘     └────────┘ └──┘ 
src                                            └──────┘       └────────┘
typ                                    └──┘└──────┘     └────────┘ └──┘ 
doc                                               └──────┘
 50  have (∃ (l : list (Σ (a : α), β a)) (i : fin (n.val)), a ∈ l ∧ array.read data i = l) ↔
id               └──┘                   └─┘  └──┘       └────────┘ └──┘     
src              └──┘                      └─┘   └──┘         └────────┘            
typ              └──┘                   └─┘  └──┘       └────────┘ └──┘     
 51    ∃ (i : fin (n.val)), a ∈ array.read data i,
id           └─┘  └──┘     └────────┘ └──┘ 
src          └─┘   └──┘      └────────┘
typ          └─┘  └──┘     └────────┘ └──┘ 
 52  by rw exists_swap; exact exists_congr (λ i, by simp),
id         └─────────┘        └──────────┘
src     └─┘└─────────┘  └────┘└──────────┘  └──┘  └──┘
typ     └─┘└─────────┘  └────┘└──────────┘  └──┘  └──┘
doc     └─┘             └────┘              └──┘  └──┘
txt     └─┘             └────┘              └──┘  └──┘
par     └─┘             └────┘              └──┘  └──┘
pid                                       └──┘  └────┘
st     └──────────────────────────────────────────┘└───┘
 53  by simp [as_list]; simpa [array.mem.def, and_comm]
id            └─────┘          └───────────┘  └──────┘
src     └────┘└─────┘  └─────┘└───────────┘└┘└──────┘└─
typ     └────┘└─────┘  └─────┘└───────────┘└┘└──────┘└─
doc     └────┘└─────┘  └─────┘             └┘        └─
txt     └────┘         └─────┘             └┘        └─
par     └────┘         └─────┘             └┘        └─
pid                                    └┘        
st     └────────────────────────────────────────────────
 54  
src  
typ  
doc  
txt  
par  
pid  
st   
 55  /-- Fold a function `f` over the key-value pairs in the bucket list -/
 56  def foldl {δ : Type w} (d : δ) (f : δ → Π a, β a → δ) : δ :=
id                                                     
typ                                                    
 57  data.foldl d (λ b d, b.foldl (λ r a, f r a.1 a.2) d)
id   └──┘└────┘        └────┘              
src      └────┘            └────┘                 
typ  └──┘└────┘        └────┘              
 58  
 59  theorem foldl_eq {δ : Type w} (d : δ) (f : δ → Π a, β a → δ) :
id                                                        
typ                                                       
 60    data.foldl d f = data.as_list.foldl (λ r a, f r a.1 a.2) d :=
id     └──┘└────┘    └──┘└──────┘└────┘              
src        └────┘          └──────┘└────┘                 
typ    └──┘└────┘    └──┘└──────┘└────┘              
doc        └────┘           └──────┘
 61  by rw [foldl, as_list, list.foldl_join, ← array.to_list_foldl]
id          └───┘  └─────┘  └─────────────┘    └─────────────────┘
src     └──┘└───┘└┘└─────┘└┘└─────────────┘└──┘└─────────────────┘└─
typ     └──┘└───┘└┘└─────┘└┘└─────────────┘└──┘└─────────────────┘└─
doc     └──┘└───┘└┘└─────┘└┘               └──┘                   └─
txt     └──┘     └┘       └┘               └──┘                   └─
par     └──┘     └┘       └┘               └──┘                   └─
pid       └┘     └┘       └┘               └──┘                   
st     └────────┘└───────┘└───────────────┘└─────────────────────┘
 62  
src  
typ  
doc  
txt  
par  
pid  
st   
 63  end
 64  end bucket_array
 65  
 66  namespace hash_map
 67  section
 68  parameters {α : Type u} {β : α → Type v} (hash_fn : α → nat)
id                  └──┘                                  └─┘
src                                                          └─┘
typ                 └──┘                                  └─┘
 69  
 70  /-- Insert the pair `⟨a, b⟩` into the correct location in the bucket array
 71    (without checking for duplication) -/
 72  def reinsert_aux {n} (data : bucket_array α β n) (a : α) (b : β a) : bucket_array α β n :=
id                                └──────────┘                      └──────────┘   
src                               └──────────┘                            └──────────┘
typ                               └──────────┘                      └──────────┘   
doc                               └──────────┘                            └──────────┘
 73  data.modify hash_fn a (λl, ⟨a, b⟩ :: l)
id   └──┘└─────┘ └─────┘           └┘ 
src      └─────┘                       └┘
typ  └──┘└─────┘ └─────┘           └┘ 
doc      └─────┘
 74  
 75  parameter [decidable_eq α]
id             └───────────┘
src             └──────────┘
typ            └───────────┘
 76  
 77  /-- Search a bucket for a key `a` and return the value -/
 78  def find_aux (a : α) : list (Σ a, β a) → option (β a)
id                         └──┘        └────┘   
src                         └──┘            └────┘
typ                        └──┘        └────┘   
 79  | []          := none
id     └┘             └──┘
src    └┘             └──┘
typ    └┘             └──┘
 80  | (⟨a',b⟩::t) := if h : a' = a then some (eq.rec_on h b) else find_aux t
id       └┘  └┘     └┘               └──┘  └───────┘          └──────┘
src           └┘      └┘                └──┘  └───────┘           └──────┘
typ      └┘  └┘     └┘               └──┘  └───────┘          └──────┘
 81  
 82  theorem find_aux_iff {a : α} {b : β a} : Π {l : list Σ a, β a}, (l.map sigma.fst).nodup → (find_aux a l = some b ↔ sigma.mk a b ∈ l)
id                                               └──┘        └──┘ └───────┘ └───┘     └──────┘    └──┘   └──────┘    
src                                                  └──┘            └──┘ └───────┘ └───┘     └──────┘      └──┘    └──────┘     
typ                                              └──┘        └──┘ └───────┘ └───┘     └──────┘    └──┘   └──────┘    
doc                                                                                   └───┘     └──────┘
 83  | []          nd := ⟨λn, by injection n, false.elim⟩
id     └┘                                   └────────┘
src    └┘                        └────────┘   └────────┘
typ    └┘                       └────────┘  └────────┘
doc                              └────────┘
txt                              └────────┘
par                              └────────┘
pid                                       
st                              └──────────┘
 84  | (⟨a',b'⟩::t) nd := begin
id             └┘
src            └┘
typ            └┘
st                        └─────
 85    by_cases a' = a,
id              └┘  
src    └───────┘  
typ    └───────┘└┘
doc    └───────┘   
txt    └───────┘   
par    └───────┘   
pid               
st   ────────────────┘└─
 86    { clear find_aux_iff, subst h,
id                                 
src      └────────────────┘  └────┘
typ      └────────────────┘  └────┘
doc      └────────────────┘  └────┘
txt      └────────────────┘  └────┘
par      └────────────────┘  └────┘
pid           └───────────┘       
st   ───┘└────────────────┘└───────┘└─
 87      suffices : b' = b ↔ b' = b ∨ sigma.mk a' b ∈ t, {simpa [find_aux, eq_comm]},
id                           └┘      └──────┘ └┘             └──────┘  └─────┘
src      └─────────┘         └──────┘       └─────┘└──────┘└┘└─────┘
typ      └─────────┘     └┘  └──────┘└┘   └─────┘└──────┘└┘└─────┘
doc      └─────────┘                          └─────┘└──────┘└┘       
txt      └─────────┘                          └─────┘        └┘       
par      └─────────┘                          └─────┘        └┘       
pid      └───────┘└┘                                       └┘       
st   ─────────────────────────────────────────────────┘└──────────────────────────┘└┘
 88      refine (or_iff_left_of_imp (λ m, _)).symm,
id               └────────────────┘
src      └─────┘ └────────────────┘  └──────────┘
typ      └─────┘ └────────────────┘  └──────────┘
doc      └─────┘                     └──────────┘
txt      └─────┘                     └──────────┘
par      └─────┘                     └──────────┘
pid                                 └─────────┘
st   ────────────────────────────────────────────┘└─
 89      have : a' ∉ t.map sigma.fst, from list.not_mem_of_nodup_cons nd,
id              └┘   └───┘ └───────┘       └────────────────────────┘ └┘
src      └─────┘   └───┘└───────┘  └───┘└────────────────────────┘
typ      └─────┘└┘ └───┘└───────┘  └───┘└────────────────────────┘└┘
doc      └─────┘                   └───┘                          
txt      └─────┘                   └───┘                          
par      └─────┘                   └───┘                          
pid      └───┘└┘                   └───┘                          
st   ──────────────────────────────┘└──────────────────────────────────┘└─
 90      exact this.elim (list.mem_map_of_mem sigma.fst m) },
id             └───────┘  └─────────────────┘ └───────┘ 
src      └────┘└───────┘ └─────────────────┘└───────┘ └┘
typ      └────┘└───────┘ └─────────────────┘└───────┘└┘
doc      └────┘                                       └┘
txt      └────┘                                       └┘
par      └────┘                                       └┘
pid                                                  
st   ─────────────────────────────────────────────────────┘└┘
 91    { have : sigma.mk a b ≠ ⟨a', b'⟩,
id              └──────┘     └┘  └┘
src      └─────┘└──────┘     └┘  
typ      └─────┘└──────┘ └┘└┘└┘
doc      └─────┘              └┘  
txt      └─────┘              └┘  
par      └─────┘              └┘  
pid      └───┘└┘              └┘  
st   ─────────────────────────────────┘└─
 92      { intro e, injection e with e, exact h e.symm },
id                                            └────┘
src        └─────┘  └────────┘ └─────┘  └────┘ └────┘
typ        └─────┘  └────────┘└─────┘  └────┘└────┘
doc        └─────┘  └────────┘ └─────┘  └────┘       
txt        └─────┘  └────────┘ └─────┘  └────┘       
par        └─────┘  └────────┘ └─────┘  └────┘       
pid             └┘            └─────┘              
st   ─────┘└─────┘└──────────────────┘└───────────────┘└┘
 93      simp at nd, simp [find_aux, h, ne.symm h, find_aux_iff, nd] }
id                         └──────┘    └─────┘                 └┘
src      └────────┘  └────┘└──────┘└┘ └┘└─────┘ └┘            └┘  └┘
typ      └────────┘  └────┘└──────┘└┘└┘└─────┘└┘└──────────┘└┘└┘└┘
doc      └────────┘  └────┘└──────┘└┘ └┘        └┘            └┘  └┘
txt      └────────┘  └────┘        └┘ └┘        └┘            └┘  └┘
par      └────────┘  └────┘        └┘ └┘        └┘            └┘  └┘
pid          └───┘              └┘ └┘        └┘            └┘  
st   ─────────────┘└────────────────────────────────────────────────┘└─
 94  end
st   ──┘
 95  
 96  /-- Returns `tt` if the bucket `l` contains the key `a` -/
 97  def contains_aux (a : α) (l : list Σ a, β a) : bool :=
id                                └──┘        └──┘
src                                └──┘           └──┘
typ                               └──┘        └──┘
 98  (find_aux a l).is_some
id    └──────┘   └─────┘
src   └──────┘     └─────┘
typ   └──────┘   └─────┘
doc   └──────┘
 99  
100  theorem contains_aux_iff {a : α} {l : list Σ a, β a} (nd : (l.map sigma.fst).nodup) : contains_aux a l ↔ a ∈ l.map sigma.fst :=
id                                        └──┘             └──┘ └───────┘ └───┘     └──────────┘      └──┘ └───────┘
src                                        └──┘                 └──┘ └───────┘ └───┘     └──────────┘          └──┘ └───────┘
typ                                       └──┘             └──┘ └───────┘ └───┘     └──────────┘      └──┘ └───────┘
doc                                                                              └───┘     └──────────┘
101  begin
st   └─────
102    unfold contains_aux,
src    └─────────────────┘
typ    └─────────────────┘
doc    └─────────────────┘
txt    └─────────────────┘
par    └─────────────────┘
pid          └───────────┘
st   ────────────────────┘└─
103    cases h : find_aux a l with b; simp,
id               └──────┘  
src    └────┘ └─┘└──────┘  └─────┘  └──┘
typ    └────┘ └─┘└──────┘└─────┘  └──┘
doc    └────┘ └─┘└──────┘  └─────┘  └──┘
txt    └────┘ └─┘          └─────┘  └──┘
par    └────┘ └─┘          └─────┘  └──┘
pid          └─┘          └─────┘
st   ────────────────────────────────────┘└─
104    { assume (b : β a) (m : sigma.mk a b ∈ l),
id                           └──────┘    
src      └──────────┘  └─────┘└──────┘   
typ      └──────────┘└─────┘└──────┘
doc      └──────────┘  └─────┘            
txt      └──────────┘  └─────┘            
par      └──────────┘  └─────┘            
pid      └──────────┘  └─────┘            
st   ───┘└─────────────────────────────────────┘└─
105      rw (find_aux_iff nd).2 m at h,
id           └──────────┘ └┘    
src      └─┘ └──────────┘  └──┘ └───┘
typ      └─┘ └──────────┘└┘└──┘└───┘
doc      └─┘               └──┘ └───┘
txt      └─┘               └──┘ └───┘
par      └─┘               └──┘ └───┘
pid                       └──┘ └───┘
st   ────────────────────────────────┘└─
106      contradiction },
src      └────────────┘
typ      └────────────┘
doc      └────────────┘
txt      └────────────┘
par      └────────────┘
pid                   
st   ─────────────────┘└┘
107    { show ∃ (b : β a), sigma.mk a b ∈ l,
id                      └──────┘      
src      └───┘└────┘  └──────┘   
typ      └───┘└────┘ └──────┘  
doc      └───┘ └────┘              
txt      └───┘ └────┘              
par      └───┘ └────┘              
pid      └───┘ └────┘              
st   ────────────────────────────────────────
108      exact ⟨_, (find_aux_iff nd).1 h⟩ },
id                  └──────────┘ └┘    
src      └────┘ └─┘ └──────────┘  └──┘ └┘
typ      └────┘ └─┘ └──────────┘└┘└──┘└┘
doc      └────┘ └─┘               └──┘ └┘
txt      └────┘ └─┘               └──┘ └┘
par      └────┘ └─┘               └──┘ └┘
pid            └─┘               └──┘ 
st   ────────────────────────────────────┘└──
109  end
st   ──┘
110  
111  /-- Modify a bucket to replace a value in the list. Leaves the list
112   unchanged if the key is not found. -/
113  def replace_aux (a : α) (b : β a) : list (Σ a, β a) → list (Σ a, β a)
id                                    └──┘        └──┘     
src                                      └──┘            └──┘    
typ                                   └──┘        └──┘     
114  | []            := []
id     └┘               └┘
src    └┘               └┘
typ    └┘               └┘
115  | (⟨a', b'⟩::t) := if a' = a then ⟨a, b⟩::t else ⟨a', b'⟩ :: replace_aux t
id       └┘  └┘ └┘                      └┘                └┘ └─────────┘
src             └┘                          └┘                └┘
typ      └┘  └┘ └┘                      └┘                └┘ └─────────┘
116  
117  /-- Modify a bucket to remove a key, if it exists. -/
118  def erase_aux (a : α) : list (Σ a, β a) → list (Σ a, β a)
id                          └──┘        └──┘     
src                          └──┘            └──┘    
typ                         └──┘        └──┘     
119  | []            := []
id     └┘               └┘
src    └┘               └┘
typ    └┘               └┘
120  | (⟨a', b'⟩::t) := if a' = a then t else ⟨a', b'⟩ :: erase_aux t
id       └┘  └┘ └┘                                  └┘ └───────┘
src             └┘                                    └┘
typ      └┘  └┘ └┘                                  └┘ └───────┘
121  
122  /-- The predicate `valid bkts sz` means that `bkts` satisfies the `hash_map`
123    invariants: There are exactly `sz` elements in it, every pair is in the
124    bucket determined by its key and the hash function, and no key appears
125    multiple times in the list. -/
126  structure valid {n} (bkts : bucket_array α β n) (sz : nat) : Prop :=
id                              └──────────┘           └─┘
src                              └──────────┘              └─┘
typ                             └──────────┘           └─┘
doc                              └──────────┘
127  (len : bkts.as_list.length = sz)
id          └──┘└──────┘└─────┘  └┘
src             └──────┘└─────┘ 
typ         └──┘└──────┘└─────┘  └┘
doc             └──────┘
128  (idx : ∀ {i} {a : Σ a, β a}, a ∈ array.read bkts i →
id                           └────────┘ └──┘ 
src                                └────────┘
typ                          └────────┘ └──┘ 
129    mk_idx n (hash_fn a.1) = i)
id     └────┘   └─────┘     
src    └────┘                
typ    └────┘   └─────┘     
doc    └────┘
130  (nodup : ∀i, ((array.read bkts i).map sigma.fst).nodup)
id                 └────────┘ └──┘  └─┘  └───────┘ └───┘
src                 └────────┘        └─┘  └───────┘ └───┘
typ                └────────┘ └──┘  └─┘  └───────┘ └───┘
doc                                                  └───┘
131  
132  theorem valid.idx_enum {n} {bkts : bucket_array α β n} {sz : nat} (v : valid bkts sz)
id                                      └──────────┘           └─┘       └───┘ └──┘ └┘
src                                     └──────────┘              └─┘       └───┘
typ                                     └──────────┘           └─┘       └───┘ └──┘ └┘
doc                                     └──────────┘                        └───┘
133    {i l} (he : (i, l) ∈ bkts.to_list.enum) {a} {b : β a} (hl : sigma.mk a b ∈ l) :
id                      └──┘└──────┘└───┘                    └──────┘    
src                           └──────┘└───┘                      └──────┘     
typ                     └──┘└──────┘└───┘                    └──────┘    
134    ∃ h, mk_idx n (hash_fn a) = ⟨i, h⟩ :=
id       └────┘   └─────┘       
src       └────┘               
typ      └────┘   └─────┘       
doc         └────┘
135  (array.mem_to_list_enum.mp he).imp (λ h e, by subst e; exact v.idx hl)
id    └────────────────────┘└─┘ └┘ └─┘                         └───┘ └┘
src   └────────────────────┘└─┘    └─┘             └────┘   └────┘└───┘
typ   └────────────────────┘└─┘ └┘ └─┘           └────┘  └────┘└───┘└┘
doc                                                └────┘   └────┘     
txt                                                └────┘   └────┘     
par                                                └────┘   └────┘     
pid                                                                  
st                                                └──────────────────────┘
136  
137  theorem valid.idx_enum_1 {n} {bkts : bucket_array α β n} {sz : nat} (v : valid bkts sz)
id                                        └──────────┘           └─┘       └───┘ └──┘ └┘
src                                       └──────────┘              └─┘       └───┘
typ                                       └──────────┘           └─┘       └───┘ └──┘ └┘
doc                                       └──────────┘                        └───┘
138    {i l} (he : (i, l) ∈ bkts.to_list.enum) {a} {b : β a} (hl : sigma.mk a b ∈ l) :
id                      └──┘└──────┘└───┘                    └──────┘    
src                           └──────┘└───┘                      └──────┘     
typ                     └──┘└──────┘└───┘                    └──────┘    
139    (mk_idx n (hash_fn a)).1 = i :=
id      └────┘   └─────┘      
src     └────┘                 
typ     └────┘   └─────┘      
doc     └────┘
140  let ⟨h, e⟩ := v.idx_enum _ he hl in by rw e; refl
id   └─┘           └───────┘   └┘ └┘          
src                 └───────┘               └─┘   └────
typ  └─┘           └───────┘   └┘ └┘       └─┘  └────
doc                                         └─┘   └────
txt                                         └─┘   └────
par                                         └─┘   └────
pid                                                  
st                                         └───────────
141  
src  
typ  
doc  
txt  
par  
pid  
st   
142  theorem valid.as_list_nodup {n} {bkts : bucket_array α β n} {sz : nat} (v : valid bkts sz) : (bkts.as_list.map sigma.fst).nodup :=
id                                           └──────────┘           └─┘       └───┘ └──┘ └┘     └──┘└──────┘└──┘ └───────┘ └───┘
src                                          └──────────┘              └─┘       └───┘                 └──────┘└──┘ └───────┘ └───┘
typ                                          └──────────┘           └─┘       └───┘ └──┘ └┘     └──┘└──────┘└──┘ └───────┘ └───┘
doc                                          └──────────┘                        └───┘                 └──────┘               └───┘
143  begin
st   └─────
144    suffices : (bkts.to_list.map (list.map sigma.fst)).pairwise list.disjoint,
id                 └──────────────┘  └──────┘ └───────┘            └───────────┘
src    └─────────┘ └──────────────┘ └──────┘└───────┘└──────────┘└───────────┘
typ    └─────────┘ └──────────────┘ └──────┘└───────┘└──────────┘└───────────┘
doc    └─────────┘                                   └──────────┘└───────────┘
txt    └─────────┘                                   └──────────┘
par    └─────────┘                                   └──────────┘
pid    └───────┘└┘                                   └──────────┘
st   ──────────────────────────────────────────────────────────────────────────┘└─
145    { simp [bucket_array.as_list, list.nodup_join, this],
id             └──────────────────┘  └─────────────┘  └──┘
src      └────┘└──────────────────┘└┘└─────────────┘└┘    
typ      └────┘└──────────────────┘└┘└─────────────┘└┘└──┘
doc      └────┘└──────────────────┘└┘               └┘    
txt      └────┘                    └┘               └┘    
par      └────┘                    └┘               └┘    
pid                              └┘               └┘    
st   ───┘└────────────────────────────────────────────────┘└─
146      change ∀ l s, array.mem s bkts → list.map sigma.fst s = l → l.nodup,
id                     └───────┘   └──┘   └──────┘ └───────┘         └────┘
src      └─────┘ └──┘ └───────┘      └──────┘└───────┘    └────┘
typ      └─────┘ └──┘ └───────┘ └──┘ └──────┘└───────┘    └────┘
doc      └─────┘ └──┘                                      └────┘
txt      └─────┘ └──┘                                     
par      └─────┘ └──┘                                     
pid             └──┘                                     
st   ──────────────────────────────────────────────────────────────────────┘└─
147      introv m e, subst e, cases m with i e, subst e,
id                                                  
src      └────────┘  └────┘   └────┘ └───────┘  └────┘
typ      └────────┘  └────┘  └────┘└───────┘  └────┘
doc      └────────┘  └────┘   └────┘ └───────┘  └────┘
txt      └────────┘  └────┘   └────┘ └───────┘  └────┘
par      └────────┘  └────┘   └────┘ └───────┘  └────┘
pid            └──┘                └───────┘       
st   ─────────────┘└───────┘└────────────────┘└───────┘└─
148      apply v.nodup },
src      └────┘       
typ      └────┘       
doc      └────┘       
txt      └────┘       
par      └────┘       
pid                  
st   ─────────────────┘└┘
149    rw [← list.enum_map_snd bkts.to_list, list.pairwise_map, list.pairwise_map],
id           └───────────────┘ └──────────┘  └───────────────┘  └───────────────┘
src    └────┘└───────────────┘└──────────┘└┘└───────────────┘└┘└───────────────┘
typ    └────┘└───────────────┘└──────────┘└┘└───────────────┘└┘└───────────────┘
doc    └────┘                             └┘                 └┘                 
txt    └────┘                             └┘                 └┘                 
par    └────┘                             └┘                 └┘                 
pid      └──┘                             └┘                 └┘                 
st   ─────────────────────────────────────┘└─────────────────┘└─────────────────┘└──
150    have : (bkts.to_list.enum.map prod.fst).nodup := by simp [list.nodup_range],
id             └───────────────────┘ └──────┘                    └──────────────┘
src    └─────┘ └───────────────────┘└──────┘└─────────┘  └────┘└──────────────┘
typ    └─────┘ └───────────────────┘└──────┘└─────────┘  └────┘└──────────────┘
doc    └─────┘                              └─────────┘  └────┘                
txt    └─────┘                              └─────────┘  └────┘                
par    └─────┘                              └─────────┘  └────┘                
pid    └───┘└┘                              └────┘└───┘  └─────┘                
st   ────────────────────────────────────────────────────┘└──────────────────────┘└─
151    refine list.pairwise.imp_of_mem _ ((list.pairwise_map _).1 this),
id            └──────────────────────┘     └───────────────┘      └──┘
src    └─────┘└──────────────────────┘└─┘  └───────────────┘└────┘    
typ    └─────┘└──────────────────────┘└─┘  └───────────────┘└────┘└──┘
doc    └─────┘                        └─┘                   └────┘    
txt    └─────┘                        └─┘                   └────┘    
par    └─────┘                        └─┘                   └────┘    
pid                                  └─┘                   └────┘    
st   ─────────────────────────────────────────────────────────────────┘└─
152    rw prod.forall, intros i l₁,
id        └─────────┘
src    └─┘└─────────┘  └─────────┘
typ    └─┘└─────────┘  └─────────┘
doc    └─┘             └─────────┘
txt    └─┘             └─────────┘
par    └─┘             └─────────┘
pid                         └───┘
st   ───────────────┘└───────────┘└─
153    rw prod.forall, intros j l₂ me₁ me₂ ij,
id        └─────────┘
src    └─┘└─────────┘  └────────────────────┘
typ    └─┘└─────────┘  └────────────────────┘
doc    └─┘             └────────────────────┘
txt    └─┘             └────────────────────┘
par    └─┘             └────────────────────┘
pid                         └──────────────┘
st   ───────────────┘└──────────────────────┘└─
154    simp [list.disjoint], intros a b ml₁ b' ml₂,
id           └───────────┘
src    └────┘└───────────┘  └───────────────────┘
typ    └────┘└───────────┘  └───────────────────┘
doc    └────┘└───────────┘  └───────────────────┘
txt    └────┘               └───────────────────┘
par    └────┘               └───────────────────┘
pid                             └─────────────┘
st   ─────────────────────┘└─────────────────────┘└─
155    apply ij, rwa [← v.idx_enum_1 _ me₁ ml₁, ← v.idx_enum_1 _ me₂ ml₂]
id                      └──────────┘   └─┘ └─┘    └──────────┘   └─┘ └─┘
src    └────┘    └─────┘└──────────┘└─┘      └──┘└──────────┘└─┘      └┘
typ    └────┘    └─────┘└──────────┘└─┘└─┘└─┘└──┘└──────────┘└─┘└─┘└─┘└┘
doc    └────┘    └─────┘            └─┘      └──┘            └─┘      └┘
txt    └────┘    └─────┘            └─┘      └──┘            └─┘      └┘
par    └────┘    └─────┘            └─┘      └──┘            └─┘      └┘
pid                └──┘            └─┘      └──┘            └─┘      
st   ─────────┘└─────────────────────────────┘└────────────────────────┘
156  end
st   └─┘
157  
158  theorem mk_as_list (n : ℕ+) : bucket_array.as_list (mk_array n.1 [] : bucket_array α β n) = [] :=
id                           └┘    └──────────────────┘  └──────┘   └┘   └──────────┘      └┘
src                          └┘    └──────────────────┘  └──────┘    └┘   └──────────┘         └┘
typ                          └┘    └──────────────────┘  └──────┘   └┘   └──────────┘      └┘
doc                          └┘    └──────────────────┘                    └──────────┘
159  list.eq_nil_iff_forall_not_mem.mpr $ λ x m,
id   └────────────────────────────┘└──┘      
src  └────────────────────────────┘└──┘
typ  └────────────────────────────┘└──┘      
160  let ⟨i, h⟩ := (bucket_array.mem_as_list _).1 m in h
id   └─┘           └──────────────────────┘     
src                 └──────────────────────┘   
typ  └─┘           └──────────────────────┘     
161  
162  theorem mk_valid (n : ℕ+) : @valid n (mk_array n.1 []) 0 :=
id                         └┘     └───┘   └──────┘   └┘
src                        └┘     └───┘    └──────┘    └┘
typ                        └┘     └───┘   └──────┘   └┘
doc                        └┘     └───┘
163  ⟨by simp [mk_as_list], λ i a h, by cases h, λ i, list.nodup_nil⟩
id             └────────┘                        └────────────┘
src      └────┘└────────┘              └────┘        └────────────┘
typ      └────┘└────────┘           └────┘      └────────────┘
doc      └────┘                        └────┘
txt      └────┘                        └────┘
par      └────┘                        └────┘
pid                                       
st      └────────────────┘             └──────┘
164  
165  theorem valid.find_aux_iff {n} {bkts : bucket_array α β n} {sz : nat} (v : valid bkts sz) {a : α} {b : β a} :
id                                          └──────────┘           └─┘       └───┘ └──┘ └┘               
src                                         └──────────┘              └─┘       └───┘
typ                                         └──────────┘           └─┘       └───┘ └──┘ └┘               
doc                                         └──────────┘                        └───┘
166    find_aux a (bkts.read hash_fn a) = some b ↔ sigma.mk a b ∈ bkts.as_list :=
id     └──────┘   └──┘└───┘ └─────┘    └──┘   └──────┘    └──┘└──────┘
src    └──────┘        └───┘             └──┘    └──────┘          └──────┘
typ    └──────┘   └──┘└───┘ └─────┘    └──┘   └──────┘    └──┘└──────┘
doc    └──────┘        └───┘                                          └──────┘
167  (find_aux_iff (v.nodup _)).trans $
id    └──────────┘  └────┘    └───┘
src   └──────────┘   └────┘    └───┘
typ   └──────────┘  └────┘    └───┘
168  by rw bkts.mem_as_list; exact ⟨λ h, ⟨_, h⟩, λ ⟨i, h⟩, (v.idx h).symm ▸ h⟩
id                                                         └───┘         
src     └─┘                  └────┘  └──┘ └─┘ └─┘ └┘ └┘ └─┘ └───┘ └─────┘ └─
typ     └─┘└──────────────┘  └────┘  └──┘ └─┘ └─┘ └┘ └┘└─┘ └───┘ └─────┘ └─
doc     └─┘                  └────┘  └──┘ └─┘ └─┘ └┘ └┘ └─┘       └─────┘  └─
txt     └─┘                  └────┘  └──┘ └─┘ └─┘ └┘ └┘ └─┘       └─────┘  └─
par     └─┘                  └────┘  └──┘ └─┘ └─┘ └┘ └┘ └─┘       └─────┘  └─
pid                                └──┘ └─┘ └─┘ └┘ └┘ └─┘       └─────┘  
st     └───────────────────────────────────────────────────────────────────────
169  
src  
typ  
doc  
txt  
par  
pid  
st   
170  theorem valid.contains_aux_iff {n} {bkts : bucket_array α β n} {sz : nat} (v : valid bkts sz) (a : α) :
id                                              └──────────┘           └─┘       └───┘ └──┘ └┘       
src                                             └──────────┘              └─┘       └───┘
typ                                             └──────────┘           └─┘       └───┘ └──┘ └┘       
doc                                             └──────────┘                        └───┘
171    contains_aux a (bkts.read hash_fn a) ↔ a ∈ bkts.as_list.map sigma.fst :=
id     └──────────┘   └──┘└───┘ └─────┘      └──┘└──────┘└──┘ └───────┘
src    └──────────┘        └───┘                    └──────┘└──┘ └───────┘
typ    └──────────┘   └──┘└───┘ └─────┘      └──┘└──────┘└──┘ └───────┘
doc    └──────────┘        └───┘                      └──────┘
172  by simp [contains_aux, option.is_some_iff_exists, v.find_aux_iff hash_fn]
id            └──────────┘  └───────────────────────┘  └────────────┘ └─────┘
src     └────┘└──────────┘└┘└───────────────────────┘└┘└────────────┘       └─
typ     └────┘└──────────┘└┘└───────────────────────┘└┘└────────────┘└─────┘└─
doc     └────┘└──────────┘└┘                         └┘                     └─
txt     └────┘            └┘                         └┘                     └─
par     └────┘            └┘                         └┘                     └─
pid                     └┘                         └┘                     
st     └───────────────────────────────────────────────────────────────────────
173  
src  
typ  
doc  
txt  
par  
pid  
st   
174  section
175    parameters {n : ℕ+} {bkts : bucket_array α β n}
id                     └┘          └──────────┘
src                    └┘          └──────────┘
typ                    └┘          └──────────┘
doc                    └┘          └──────────┘
176               {bidx : fin n.1} {f : list (Σ a, β a) → list (Σ a, β a)}
id                        └─┘          └──┘          └──┘      
src                       └─┘          └──┘            └──┘    
typ                       └─┘          └──┘          └──┘      
177               (u v1 v2 w : list Σ a, β a)
id                             └──┘     
src                            └──┘   
typ                            └──┘     
178  
179    local notation `L` := array.read bkts bidx
id                           └────────┘
src                          └────────┘
typ                          └────────┘
180    private def bkts' : bucket_array α β n := array.write bkts bidx (f L)
id                         └──────────┘       └─────────┘ └──┘ └──┘   
src                        └──────────┘          └─────────┘              
typ                        └──────────┘       └─────────┘ └──┘ └──┘   
doc                        └──────────┘
181  
182    variables (hl : L = u ++ v1 ++ w)
id                         └┘    └┘
src                        └┘    └┘
typ                        └┘    └┘
183              (hfl : f L = u ++ v2 ++ w)
id                            └┘    └┘
src                           └┘    └┘
typ                           └┘    └┘
184    include hl hfl
185  
186    theorem append_of_modify : ∃ u' w', bkts.as_list = u' ++ v1 ++ w' ∧ bkts'.as_list = u' ++ v2 ++ w' :=
id                                 └┘ └┘ └──┘└──────┘  └┘ └┘ └┘ └┘ └┘  └───┘└──────┘  └┘ └┘ └┘ └┘ └┘
src                                          └──────┘     └┘    └┘     └───┘└──────┘     └┘    └┘
typ                                └┘ └┘ └──┘└──────┘  └┘ └┘ └┘ └┘ └┘  └───┘└──────┘  └┘ └┘ └┘ └┘ └┘
doc                                            └──────┘                         └──────┘
187    begin
st     └─────
188      unfold bucket_array.as_list,
src      └─────────────────────────┘
typ      └─────────────────────────┘
doc      └─────────────────────────┘
txt      └─────────────────────────┘
par      └─────────────────────────┘
pid            └───────────────────┘
st   ──────────────────────────────┘└─
189      have h : bidx.1 < bkts.to_list.length, {simp [bidx.2]},
id                └──┘    └─────────────────┘         └──┘
src      └───────┘    └─┘└─────────────────┘   └────┘    └─┘
typ      └───────┘└──┘└─┘└─────────────────┘   └────┘└──┘└─┘
doc      └───────┘    └─┘                       └────┘    └─┘
txt      └───────┘    └─┘                       └────┘    └─┘
par      └───────┘    └─┘                       └────┘    └─┘
pid      └────┘└─┘    └─┘                               └─┘
st   ────────────────────────────────────────┘└──────────────┘└┘
190      refine ⟨(bkts.to_list.take bidx.1).join ++ u, w ++ (bkts.to_list.drop (bidx.1+1)).join, _, _⟩,
id                └───────────────┘              └┘        └───────────────┘  └──┘  
src      └─────┘  └───────────────┘    └───────┘└┘ └┘    └───────────────┘     └┘└─────────────┘
typ      └─────┘  └───────────────┘    └───────┘└┘└┘   └───────────────┘ └──┘└┘└─────────────┘
doc      └─────┘                       └───────┘   └┘                          └┘ └─────────────┘
txt      └─────┘                       └───────┘   └┘                          └┘ └─────────────┘
par      └─────┘                       └───────┘   └┘                          └┘ └─────────────┘
pid                                   └───────┘   └┘                          └┘ └─────────────┘
st   ────────────────────────────────────────────────────────────────────────────────────────────────┘└─
191      { conv { to_lhs,
src        └─────┘└────┘└─
typ        └─────┘└────┘└─
txt        └─────┘└────┘└─
par        └─────┘└────┘└─
pid            └─────────
st   ─────┘└────┘└─────┘└─
192          rw [← list.take_append_drop bidx.1 bkts.to_list, list.drop_eq_nth_le_cons h],
id                 └───────────────────┘ └──┘   └──────────┘  └──────────────────────┘ 
src  ───────┘└────┘└───────────────────┘    └─┘└──────────┘└┘└──────────────────────┘ └─
typ  ───────┘└────┘└───────────────────┘└──┘└─┘└──────────┘└┘└──────────────────────┘└─
txt  ───────┘└────┘                         └─┘            └┘                         └─
par  ───────┘└────┘                         └─┘            └┘                         └─
pid  ─────────────┘                         └─┘            └┘                         └──
st   ──────────────────────────────────────────────────────┘└──────────────────────────┘ └─
193          simp [hl] }, simp },
id                 └┘
src  ───────┘└────┘  └┘  └───┘
typ  ───────┘└────┘└┘└┘  └───┘
doc                       └───┘
txt  ───────┘└────┘  └┘  └───┘
par  ───────┘└────┘  └┘  └───┘
pid  ─────────────┘  └─┘      
st   ─────────────────┘└┘└────┘└┘
194      { conv { to_lhs,
src        └─────┘└────┘└─
typ        └─────┘└────┘└─
txt        └─────┘└────┘└─
par        └─────┘└────┘└─
pid            └─────────
st   ───────────┘└─────┘└─
195          rw [bkts', array.write_to_list, list.update_nth_eq_take_cons_drop _ h],
id               └───┘  └─────────────────┘  └───────────────────────────────┘   
src  ───────┘└──┘└───┘└┘└─────────────────┘└┘└───────────────────────────────┘└─┘ └─
typ  ───────┘└──┘└───┘└┘└─────────────────┘└┘└───────────────────────────────┘└─┘└─
txt  ───────┘└──┘     └┘                   └┘                                 └─┘ └─
par  ───────┘└──┘     └┘                   └┘                                 └─┘ └─
pid  ───────────┘     └┘                   └┘                                 └─┘ └──
st   ────────────────┘└───────────────────┘└─────────────────────────────────────┘ └─
196          simp [hfl] }, simp }
id                 └─┘
src  ───────┘└────┘   └┘  └───┘
typ  ───────┘└────┘└─┘└┘  └───┘
doc                        └───┘
txt  ───────┘└────┘   └┘  └───┘
par  ───────┘└────┘   └┘  └───┘
pid  ─────────────┘   └─┘      
st   ──────────────────┘└┘└────┘└─
197    end
st   ────┘
198  
199    variables (hvnd : (v2.map sigma.fst).nodup)
id                          └──┘ └───────┘ └───┘
src                         └──┘ └───────┘ └───┘
typ                         └──┘ └───────┘ └───┘
doc                                        └───┘
200              (hal : ∀ (a : Σ a, β a), a ∈ v2 → mk_idx n (hash_fn a.1) = bidx)
id                                           └────┘               
src                                             └────┘                
typ                                          └────┘               
doc                                                └────┘
201              (djuv : (u.map sigma.fst).disjoint (v2.map sigma.fst))
id                         └──┘ └───────┘ └──────┘     └──┘ └───────┘
src                        └──┘ └───────┘ └──────┘     └──┘ └───────┘
typ                        └──┘ └───────┘ └──────┘     └──┘ └───────┘
doc                                       └──────┘
202              (djwv : (w.map sigma.fst).disjoint (v2.map sigma.fst))
id                         └──┘ └───────┘ └──────┘     └──┘ └───────┘
src                        └──┘ └───────┘ └──────┘     └──┘ └───────┘
typ                        └──┘ └───────┘ └──────┘     └──┘ └───────┘
doc                                       └──────┘
203    include hvnd hal djuv djwv
204  
205    theorem valid.modify {sz : ℕ} (v : valid bkts sz) : sz + v2.length ≥ v1.length ∧ valid bkts' (sz + v2.length - v1.length) :=
id                                       └───┘ └──┘ └┘    └┘  └┘└─────┘  └┘└─────┘  └───┘ └───┘  └┘  └┘└─────┘  └┘└─────┘
src                                      └───┘                  └─────┘    └─────┘  └───┘ └───┘        └─────┘    └─────┘
typ                                      └───┘ └──┘ └┘    └┘  └┘└─────┘  └┘└─────┘  └───┘ └───┘  └┘  └┘└─────┘  └┘└─────┘
doc                                       └───┘                                         └───┘
206    begin
st     └─────
207      rcases append_of_modify u v1 v2 w hl hfl with ⟨u', w', e₁, e₂⟩,
id              └──────────────┘  └┘ └┘  └┘ └─┘
src      └─────┘└──────────────┘           └────────────────────┘
typ      └─────┘└──────────────┘└┘└┘└┘└─┘└────────────────────┘
doc      └─────┘                           └────────────────────┘
txt      └─────┘                           └────────────────────┘
par      └─────┘                           └────────────────────┘
pid                                       └────────────────────┘
st   ─────────────────────────────────────────────────────────────────┘└─
208      rw [← v.len, e₁],
id                    └┘
src      └────┘     └┘  
typ      └────┘└───┘└┘└┘
doc      └────┘     └┘  
txt      └────┘     └┘  
par      └────┘     └┘  
pid        └──┘     └┘  
st   ──────────────┘└──┘└──
209      suffices : valid bkts' (u' ++ v2 ++ w').length,
id                        └───┘  └┘ └┘ └┘    └┘
src      └─────────┘     └───┘   └┘      └──────┘
typ      └─────────┘     └───┘ └┘└┘└┘  └┘└──────┘
doc      └─────────┘                     └──────┘
txt      └─────────┘                     └──────┘
par      └─────────┘                     └──────┘
pid      └───────┘└┘                     └─────┘
st   ─────────────────────────────────────────────────┘└─
210      { simpa [ge, nat.le_add_right, nat.add_sub_cancel_left] },
id                └┘  └──────────────┘  └─────────────────────┘
src        └─────┘└┘└┘└──────────────┘└┘└─────────────────────┘└┘
typ        └─────┘└┘└┘└──────────────┘└┘└─────────────────────┘└┘
doc        └─────┘  └┘                └┘                       └┘
txt        └─────┘  └┘                └┘                       └┘
par        └─────┘  └┘                └┘                       └┘
pid               └┘                └┘                       
st   ─────┘└────────────────────────────────────────────────────┘└┘
211      refine ⟨congr_arg _ e₂, λ i a, _, λ i, _⟩,
id               └───────┘   └┘
src      └─────┘ └───────┘└─┘  └┘ └───────┘ └────┘
typ      └─────┘ └───────┘└─┘└┘└┘ └───────┘ └────┘
doc      └─────┘          └─┘  └┘ └───────┘ └────┘
txt      └─────┘          └─┘  └┘ └───────┘ └────┘
par      └─────┘          └─┘  └┘ └───────┘ └────┘
pid                      └─┘  └┘ └───────┘ └────┘
st   ────────────────────────────────────────────┘└─
212      { by_cases bidx = i,
id                  └──┘  
src        └───────┘    
typ        └───────┘└──┘
doc        └───────┘     
txt        └───────┘     
par        └───────┘     
pid                     
st   ─────┘└───────────────┘└─
213        { subst i, rw [bkts', array.read_write, hfl],
id                       └───┘  └──────────────┘  └─┘
src          └────┘   └──┘└───┘└┘└──────────────┘└┘   
typ          └────┘  └──┘└───┘└┘└──────────────┘└┘└─┘
doc          └────┘   └──┘     └┘                └┘   
txt          └────┘   └──┘     └┘                └┘   
par          └────┘   └──┘     └┘                └┘   
pid                    └┘     └┘                └┘   
st   ───────┘└─────┘└─────────┘└────────────────┘└───┘└──
214          have := @valid.idx _ _ _ v bidx a,
id                                     └──┘ 
src          └──────┘          └─────┘     
typ          └──────┘          └─────┘└──┘
doc          └──────┘          └─────┘     
txt          └──────┘          └─────┘     
par          └──────┘          └─────┘     
pid          └───┘└─┘          └─────┘     
st   ────────────────────────────────────────┘└─
215          simp only [hl, list.mem_append, or_imp_distrib, forall_and_distrib] at this ⊢,
id                      └┘  └─────────────┘  └────────────┘  └────────────────┘
src          └─────────┘  └┘└─────────────┘└┘└────────────┘└┘└────────────────┘└─────────┘
typ          └─────────┘└┘└┘└─────────────┘└┘└────────────┘└┘└────────────────┘└─────────┘
doc          └─────────┘  └┘               └┘              └┘                  └─────────┘
txt          └─────────┘  └┘               └┘              └┘                  └─────────┘
par          └─────────┘  └┘               └┘              └┘                  └─────────┘
pid              └──┘└┘  └┘               └┘              └┘                  └───────┘
st   ────────────────────────────────────────────────────────────────────────────────────┘└─
216          exact ⟨⟨this.1.1, hal _⟩, this.2⟩ },
id                             └─┘     └──┘
src          └────┘      └────┘   └───┘    └──┘
typ          └────┘      └────┘└─┘└───┘└──┘└──┘
doc          └────┘      └────┘   └───┘    └──┘
txt          └────┘      └────┘   └───┘    └──┘
par          └────┘      └────┘   └───┘    └──┘
pid                     └────┘   └───┘    └─┘
st   ─────────────────────────────────────────┘└┘
217        { rw [bkts', array.read_write_of_ne _ _ h], apply v.idx } },
id               └───┘  └────────────────────┘     
src          └──┘└───┘└┘└────────────────────┘└───┘   └────┘     
typ          └──┘└───┘└┘└────────────────────┘└───┘  └────┘     
doc          └──┘     └┘                      └───┘   └────┘     
txt          └──┘     └┘                      └───┘   └────┘     
par          └──┘     └┘                      └───┘   └────┘     
pid            └┘     └┘                      └───┘             
st   ────────────────┘└────────────────────────────┘└─────────────┘└──┘
218      { by_cases bidx = i,
id                  └──┘   
src        └───────┘     
typ        └───────┘└──┘ 
doc        └───────┘     
txt        └───────┘     
par        └───────┘     
pid                     
st   ──────────────────────┘└─
219        { subst i, rw [bkts', array.read_write, hfl],
id                       └───┘  └──────────────┘  └─┘
src          └────┘   └──┘└───┘└┘└──────────────┘└┘   
typ          └────┘  └──┘└───┘└┘└──────────────┘└┘└─┘
doc          └────┘   └──┘     └┘                └┘   
txt          └────┘   └──┘     └┘                └┘   
par          └────┘   └──┘     └┘                └┘   
pid                    └┘     └┘                └┘   
st   ───────┘└─────┘└─────────┘└────────────────┘└───┘└──
220          have := @valid.nodup _ _ _ v bidx,
id                                       └──┘
src          └──────┘            └─────┘ 
typ          └──────┘            └─────┘└──┘
doc          └──────┘            └─────┘ 
txt          └──────┘            └─────┘ 
par          └──────┘            └─────┘ 
pid          └───┘└─┘            └─────┘ 
st   ────────────────────────────────────────┘└─
221          simp [hl, list.nodup_append] at this,
id                 └┘  └───────────────┘
src          └────┘  └┘└───────────────┘└───────┘
typ          └────┘└┘└┘└───────────────┘└───────┘
doc          └────┘  └┘                 └───────┘
txt          └────┘  └┘                 └───────┘
par          └────┘  └┘                 └───────┘
pid                └┘                 └─────┘
st   ───────────────────────────────────────────┘└─
222          simp [list.nodup_append, this, hvnd, djuv, djwv.symm] },
id                 └───────────────┘  └──┘  └──┘  └──┘
src          └────┘└───────────────┘└┘    └┘    └┘    └┘         └┘
typ          └────┘└───────────────┘└┘└──┘└┘└──┘└┘└──┘└┘└───────┘└┘
doc          └────┘                 └┘    └┘    └┘    └┘         └┘
txt          └────┘                 └┘    └┘    └┘    └┘         └┘
par          └────┘                 └┘    └┘    └┘    └┘         └┘
pid                               └┘    └┘    └┘    └┘         
st   ─────────────────────────────────────────────────────────────┘└┘
223        { rw [bkts', array.read_write_of_ne _ _ h], apply v.nodup } }
id               └───┘  └────────────────────┘     
src          └──┘└───┘└┘└────────────────────┘└───┘   └────┘       
typ          └──┘└───┘└┘└────────────────────┘└───┘  └────┘       
doc          └──┘     └┘                      └───┘   └────┘       
txt          └──┘     └┘                      └───┘   └────┘       
par          └──┘     └┘                      └───┘   └────┘       
pid            └┘     └┘                      └───┘               
st   ────────────────┘└────────────────────────────┘└───────────────┘└───
224    end
st   ────┘
225  end
226  
227  theorem valid.replace_aux (a : α) (b : β a) : Π (l : list (Σ a, β a)), a ∈ l.map sigma.fst →
id                                                    └──┘           └──┘ └───────┘
src                                                       └──┘                └──┘ └───────┘
typ                                                   └──┘           └──┘ └───────┘
228    ∃ (u w : list Σ a, β a) b', l = u ++ [⟨a, b'⟩] ++ w ∧ replace_aux a b l = u ++ [⟨a, b⟩] ++ w
id             └──┘      └┘    └┘    └┘  └┘   └─────────┘      └┘      └┘ 
src            └──┘                 └┘         └┘    └─────────┘          └┘        └┘
typ            └──┘      └┘    └┘    └┘  └┘   └─────────┘      └┘      └┘ 
doc                                                          └─────────┘
229  | []            := false.elim
id     └┘               └────────┘
src    └┘               └────────┘
typ    └┘               └────────┘
230  | (⟨a', b'⟩::t) := begin
id              └┘
src             └┘
typ             └┘
st                      └─────
231    by_cases e : a' = a,
id                  └┘  
src    └───────┘ └─┘  
typ    └───────┘ └─┘└┘
doc    └───────┘ └─┘   
txt    └───────┘ └─┘   
par    └───────┘ └─┘   
pid             └─┘   
st   ────────────────────┘└─
232    { subst a',
id             └┘
src      └────┘
typ      └────┘└┘
doc      └────┘
txt      └────┘
par      └────┘
pid           
st   ───┘└──────┘└─
233      suffices : ∃ (u w : list Σ a, β a) (b'' : β a),
id                          └──┘                   
src      └─────────┘└──────┘└──┘└┘  └───────┘  
typ      └─────────┘└──────┘└──┘└┘  └───────┘ 
doc      └─────────┘ └──────┘     └┘   └───────┘   
txt      └─────────┘ └──────┘     └┘   └───────┘   
par      └─────────┘ └──────┘     └┘   └───────┘   
pid      └───────┘└┘ └──────┘     └┘   └───────┘   
st   ────────────────────────────────────────────────────
234        (sigma.mk a b') :: t = u ++ ⟨a, b''⟩ :: w ∧
id          └──────┘                └┘
src  ─────┘ └──────┘   └┘     └┘  └┘   └┘    
typ  ─────┘ └──────┘   └┘     └┘  └┘   └┘    
doc  ─────┘            └┘         └┘   └┘    
txt  ─────┘            └┘         └┘   └┘    
par  ─────┘            └┘         └┘   └┘    
pid  ─────┘            └┘         └┘   └┘    
st   ──────────────────────────────────────────────────
235        replace_aux a b (⟨a, b'⟩ :: t) = u ++ ⟨a, b⟩ :: w, {simpa},
id         └─────────┘          └┘                 
src  ─────┘└─────────┘     └┘  └┘   └┘      └┘ └┘      └───┘
typ  ─────┘└─────────┘     └┘└┘└┘  └┘     └┘└┘      └───┘
doc  ─────┘└─────────┘     └┘  └┘   └┘      └┘ └┘      └───┘
txt  ─────┘                └┘  └┘   └┘      └┘ └┘      └───┘
par  ─────┘                └┘  └┘   └┘      └┘ └┘      └───┘
pid  ─────┘                └┘  └┘   └┘      └┘ └┘  
st   ──────────────────────────────────────────────────────┘└──────┘└┘
236      refine ⟨[], t, b', _⟩, simp [replace_aux] },
id                     └┘            └─────────┘
src      └─────┘   └┘ └┘  └──┘  └────┘└─────────┘└┘
typ      └─────┘   └┘└┘└┘└──┘  └────┘└─────────┘└┘
doc      └─────┘   └┘ └┘  └──┘  └────┘└─────────┘└┘
txt      └─────┘   └┘ └┘  └──┘  └────┘           └┘
par      └─────┘   └┘ └┘  └──┘  └────┘           └┘
pid               └┘ └┘  └──┘                 
st   ────────────────────────┘└───────────────────┘└┘
237    { suffices : ∀ (x : β a) (_ : sigma.mk a x ∈ t), ∃ u w (b'' : β a),
id                                                                    
src      └─────────┘ └────┘  └─────┘            └──────────┘  
typ      └─────────┘ └────┘  └─────┘            └──────────┘ 
doc      └─────────┘ └────┘  └─────┘              └──────────┘   
txt      └─────────┘ └────┘  └─────┘              └──────────┘   
par      └─────────┘ └────┘  └─────┘              └──────────┘   
pid      └───────┘└┘ └────┘  └─────┘              └──────────┘   
st   ──────────────────────────────────────────────────────────────────────
238        (sigma.mk a' b') :: t = u ++ ⟨a, b''⟩ :: w ∧
src  ─────┘             └┘         └┘   └┘    
typ  ─────┘             └┘         └┘   └┘    
doc  ─────┘             └┘         └┘   └┘    
txt  ─────┘             └┘         └┘   └┘    
par  ─────┘             └┘         └┘   └┘    
pid  ─────┘             └┘         └┘   └┘    
st   ───────────────────────────────────────────────────
239        (sigma.mk a' b') :: (replace_aux a b t) = u ++ ⟨a, b⟩ :: w,
id          └──────┘ └┘ └┘      └─────────┘                 
src  ─────┘ └──────┘    └┘   └─────────┘   └┘      └┘ └┘  
typ  ─────┘ └──────┘└┘└┘└┘   └─────────┘  └┘     └┘└┘  
doc  ─────┘             └┘   └─────────┘   └┘      └┘ └┘  
txt  ─────┘             └┘                 └┘      └┘ └┘  
par  ─────┘             └┘                 └┘      └┘ └┘  
pid  ─────┘             └┘                 └┘      └┘ └┘  
st   ───────────────────────────────────────────────────────────────┘└─
240      { simpa [replace_aux, ne.symm e, e] },
id                └─────────┘  └─────┘   
src        └─────┘└─────────┘└┘└─────┘ └┘ └┘
typ        └─────┘└─────────┘└┘└─────┘└┘└┘
doc        └─────┘└─────────┘└┘        └┘ └┘
txt        └─────┘           └┘        └┘ └┘
par        └─────┘           └┘        └┘ └┘
pid                        └┘        └┘ 
st   ─────┘└────────────────────────────────┘└┘
241      intros x m,
src      └────────┘
typ      └────────┘
doc      └────────┘
txt      └────────┘
par      └────────┘
pid            └──┘
st   ─────────────┘└─
242      have IH : ∀ (x : β a) (_ : sigma.mk a x ∈ t), ∃ u w (b'' : β a),
id                                  └──────┘                          
src      └────────┘ └────┘  └─────┘└──────┘     └──────────┘  
typ      └────────┘ └────┘  └─────┘└──────┘     └──────────┘ 
doc      └────────┘ └────┘  └─────┘              └──────────┘   
txt      └────────┘ └────┘  └─────┘              └──────────┘   
par      └────────┘ └────┘  └─────┘              └──────────┘   
pid      └─────┘└─┘ └────┘  └─────┘              └──────────┘   
st   ─────────────────────────────────────────────────────────────────────
243        t = u ++ ⟨a, b''⟩ :: w ∧ replace_aux a b t = u ++ ⟨a, b⟩ :: w,
id                                  └─────────┘                
src  ─────┘       └┘   └┘    └─────────┘         └┘ └┘  
typ  ─────┘       └┘   └┘    └─────────┘       └┘└┘  
doc  ─────┘       └┘   └┘    └─────────┘         └┘ └┘  
txt  ─────┘       └┘   └┘                        └┘ └┘  
par  ─────┘       └┘   └┘                        └┘ └┘  
pid  ─────┘       └┘   └┘                        └┘ └┘  
st   ──────────────────────────────────────────────────────────────────┘└─
244      { simpa using valid.replace_aux t },
id                     └───────────────┘ 
src        └──────────┘                  
typ        └──────────┘└───────────────┘
doc        └──────────┘                  
txt        └──────────┘                  
par        └──────────┘                  
pid             └────┘                  
st   ─────┘└──────────────────────────────┘└┘
245      rcases IH x m with ⟨u, w, b'', hl, hfl⟩,
id              └┘  
src      └─────┘    └────────────────────────┘
typ      └─────┘└┘└────────────────────────┘
doc      └─────┘    └────────────────────────┘
txt      └─────┘    └────────────────────────┘
par      └─────┘    └────────────────────────┘
pid                └────────────────────────┘
st   ──────────────────────────────────────────┘└─
246      exact ⟨⟨a', b'⟩ :: u, w, b'', by simp [hl, hfl.symm, ne.symm e]⟩ }
id               └┘  └┘         └─┘           └┘            └─────┘ 
src      └────┘    └┘  └┘   └┘ └┘   └┘  └────┘  └┘        └┘└─────┘ └┘
typ      └────┘  └┘└┘└┘└┘  └┘└┘└─┘└┘  └────┘└┘└┘└──────┘└┘└─────┘└┘
doc      └────┘    └┘  └┘   └┘ └┘   └┘  └────┘  └┘        └┘        └┘
txt      └────┘    └┘  └┘   └┘ └┘   └┘  └────┘  └┘        └┘        └┘
par      └────┘    └┘  └┘   └┘ └┘   └┘  └────┘  └┘        └┘        └┘
pid               └┘  └┘   └┘ └┘   └┘  └─────┘  └┘        └┘        └┘
st   ───────────────────────────────────┘└─────────────────────────────┘└┘└─
247  end
st   ──┘
248  
249  theorem valid.replace {n : ℕ+}
id                              └┘
src                             └┘
typ                             └┘
doc                             └┘
250    {bkts : bucket_array α β n} {sz : ℕ} (a : α) (b : β a)
id             └──────────┘                          
src            └──────────┘              
typ            └──────────┘                          
doc            └──────────┘
251    (Hc : contains_aux a (bkts.read hash_fn a))
id           └──────────┘   └──┘└───┘ └─────┘ 
src          └──────────┘        └───┘
typ          └──────────┘   └──┘└───┘ └─────┘ 
doc          └──────────┘        └───┘
252    (v : valid bkts sz) : valid (bkts.modify hash_fn a (replace_aux a b)) sz :=
id          └───┘ └──┘ └┘    └───┘  └──┘└─────┘ └─────┘   └─────────┘     └┘
src         └───┘            └───┘      └─────┘            └─────────┘
typ         └───┘ └──┘ └┘    └───┘  └──┘└─────┘ └─────┘   └─────────┘     └┘
doc         └───┘            └───┘      └─────┘            └─────────┘
253  begin
st   └─────
254    have nd := v.nodup (mk_idx n (hash_fn a)),
id                └─────┘  └────┘   └─────┘ 
src    └─────────┘└─────┘ └────┘          └┘
typ    └─────────┘└─────┘ └────┘ └─────┘└┘
doc    └─────────┘        └────┘          └┘
txt    └─────────┘                        └┘
par    └─────────┘                        └┘
pid    └─────┘└─┘                        └┘
st   ──────────────────────────────────────────┘└─
255    rcases hash_map.valid.replace_aux a b (array.read bkts (mk_idx n (hash_fn a)))
id                                           └────────┘ └──┘  └────┘   └─────┘ 
src    └─────┘                             └────────┘     └────┘          └───
typ    └─────┘                            └────────┘└──┘ └────┘ └─────┘└───
doc    └─────┘                                            └────┘          └───
txt    └─────┘                                                            └───
par    └─────┘                                                            └───
pid                                                                      └───
st   ─────────────────────────────────────────────────────────────────────────────────
256      ((contains_aux_iff nd).1 Hc) with ⟨u, w, b', hl, hfl⟩,
id         └──────────────┘ └┘    └┘
src  ───┘  └──────────────┘  └──┘  └────────────────────────┘
typ  ───┘  └──────────────┘└┘└──┘└┘└────────────────────────┘
doc  ───┘                    └──┘  └────────────────────────┘
txt  ───┘                    └──┘  └────────────────────────┘
par  ───┘                    └──┘  └────────────────────────┘
pid  ───┘                    └──┘  └────────────────────────┘
st   ────────────────────────────────────────────────────────┘└─
257    simp [hl, list.nodup_append] at nd,
id           └┘  └───────────────┘
src    └────┘  └┘└───────────────┘└─────┘
typ    └────┘└┘└┘└───────────────┘└─────┘
doc    └────┘  └┘                 └─────┘
txt    └────┘  └┘                 └─────┘
par    └────┘  └┘                 └─────┘
pid          └┘                 └───┘
st   ───────────────────────────────────┘└─
258    refine (v.modify hash_fn
id             └──────┘ └─────┘
src    └─────┘ └──────┘       
typ    └─────┘ └──────┘└─────┘
doc    └─────┘                
txt    └─────┘                
par    └─────┘                
pid                          
st   ───────────────────────────
259      u [⟨a, b'⟩] [⟨a, b⟩] w hl hfl (list.nodup_singleton _)
id             └┘           └┘ └─┘  └──────────────────┘
src  ───┘    └┘      └┘         └──────────────────┘└───
typ  ───┘   └┘└┘   └┘ └┘└─┘ └──────────────────┘└───
doc  ───┘    └┘      └┘                             └───
txt  ───┘    └┘      └┘                             └───
par  ───┘    └┘      └┘                             └───
pid  ───┘    └┘      └┘                             └───
st   ───────────────────────────────────────────────────────────
260      (λa' e, by simp at e; rw e)
id                                
src  ───┘  └────┘  └───────┘└┘└─┘ └─
typ  ───┘  └────┘  └───────┘└┘└─┘└─
doc  ───┘  └────┘  └───────┘└┘└─┘ └─
txt  ───┘  └────┘  └───────┘└┘└─┘ └─
par  ───┘  └────┘  └───────┘└┘└─┘ └─
pid  ───┘  └────┘  └─────────────┘ └─
st   ─────────────┘└─────────────┘└─
261      (λa' e1 e2, _)
src  ───┘  └────────────
typ  ───┘  └────────────
doc  ───┘  └────────────
txt  ───┘  └────────────
par  ───┘  └────────────
pid  ───┘  └────────────
st   ───────────────────
262      (λa' e1 e2, _)).2;
src  ───┘  └─────────────┘
typ  ───┘  └─────────────┘
doc  ───┘  └─────────────┘
txt  ───┘  └─────────────┘
par  ───┘  └─────────────┘
pid  ───┘  └───────────┘└┘
st   ───────────────────────
263    { revert e1, simp [-sigma.exists] at e2, subst a', simp [nd] }
id                                                    └┘        └┘
src      └───────┘  └────────────────────────┘  └────┘    └────┘  └┘
typ      └───────┘  └────────────────────────┘  └────┘└┘  └────┘└┘└┘
doc      └───────┘  └────────────────────────┘  └────┘    └────┘  └┘
txt      └───────┘  └────────────────────────┘  └────┘    └────┘  └┘
par      └───────┘  └────────────────────────┘  └────┘    └────┘  └┘
pid            └─┘      └─────────────┘└───┘                 
st   ─┘└─────────┘└──────────────────────────┘└────────┘└──────────┘└─
264  end
st   ──┘
265  
266  theorem valid.insert {n : ℕ+}
id                             └┘
src                            └┘
typ                            └┘
doc                            └┘
267    {bkts : bucket_array α β n} {sz : ℕ} (a : α) (b : β a)
id             └──────────┘                          
src            └──────────┘              
typ            └──────────┘                          
doc            └──────────┘
268    (Hnc : ¬ contains_aux a (bkts.read hash_fn a))
id             └──────────┘   └──┘└───┘ └─────┘ 
src            └──────────┘        └───┘
typ            └──────────┘   └──┘└───┘ └─────┘ 
doc             └──────────┘        └───┘
269    (v : valid bkts sz) : valid (reinsert_aux bkts a b) (sz+1) :=
id          └───┘ └──┘ └┘    └───┘  └──────────┘ └──┘     └┘
src         └───┘            └───┘  └──────────┘              
typ         └───┘ └──┘ └┘    └───┘  └──────────┘ └──┘     └┘
doc         └───┘            └───┘  └──────────┘
270  begin
st   └─────
271    have nd := v.nodup (mk_idx n (hash_fn a)),
id                └─────┘  └────┘   └─────┘ 
src    └─────────┘└─────┘ └────┘          └┘
typ    └─────────┘└─────┘ └────┘ └─────┘└┘
doc    └─────────┘        └────┘          └┘
txt    └─────────┘                        └┘
par    └─────────┘                        └┘
pid    └─────┘└─┘                        └┘
st   ──────────────────────────────────────────┘└─
272    refine (v.modify hash_fn
id             └──────┘
src    └─────┘ └──────┘       
typ    └─────┘ └──────┘       
doc    └─────┘                
txt    └─────┘                
par    └─────┘                
pid                          
st   ───────────────────────────
273      [] [] [⟨a, b⟩] (bkts.read hash_fn a) rfl rfl (list.nodup_singleton _)
id                      └───────┘ └─────┘       └─┘  └──────────────────┘
src  ───┘       └┘   └───────┘        └┘   └─┘ └──────────────────┘└───
typ  ───┘       └┘  └───────┘└─────┘└┘   └─┘ └──────────────────┘└───
doc  ───┘       └┘   └───────┘        └┘                           └───
txt  ───┘       └┘                    └┘                           └───
par  ───┘       └┘                    └┘                           └───
pid  ───┘       └┘                    └┘                           └───
st   ──────────────────────────────────────────────────────────────────────────
274      (λa' e, by simp at e; rw e)
id                                
src  ───┘  └────┘  └───────┘└┘└─┘ └─
typ  ───┘  └────┘  └───────┘└┘└─┘└─
doc  ───┘  └────┘  └───────┘└┘└─┘ └─
txt  ───┘  └────┘  └───────┘└┘└─┘ └─
par  ───┘  └────┘  └───────┘└┘└─┘ └─
pid  ───┘  └────┘  └─────────────┘ └─
st   ─────────────┘└─────────────┘└─
275      (λa', false.elim)
id             └────────┘
src  ───┘  └──┘└────────┘└─
typ  ───┘  └──┘└────────┘└─
doc  ───┘  └──┘          └─
txt  ───┘  └──┘          └─
par  ───┘  └──┘          └─
pid  ───┘  └──┘          └─
st   ──────────────────────
276      (λa' e1 e2, _)).2,
src  ───┘  └─────────────┘
typ  ───┘  └─────────────┘
doc  ───┘  └─────────────┘
txt  ───┘  └─────────────┘
par  ───┘  └─────────────┘
pid  ───┘  └───────────┘└┘
st   ────────────────────┘└─
277    simp [-sigma.exists] at e2, subst a',
id                                       └┘
src    └────────────────────────┘  └────┘
typ    └────────────────────────┘  └────┘└┘
doc    └────────────────────────┘  └────┘
txt    └────────────────────────┘  └────┘
par    └────────────────────────┘  └────┘
pid        └─────────────┘└───┘       
st   ───────────────────────────┘└────────┘└─
278    exact Hnc ((contains_aux_iff nd).2 e1)
id           └─┘   └──────────────┘ └┘    └┘
src    └────┘     └──────────────┘  └──┘  └┘
typ    └────┘└─┘  └──────────────┘└┘└──┘└┘└┘
doc    └────┘                       └──┘  └┘
txt    └────┘                       └──┘  └┘
par    └────┘                       └──┘  └┘
pid                                └──┘  
st   ────────────────────────────────────────┘
279  end
st   └─┘
280  
281  theorem valid.erase_aux (a : α) : Π (l : list (Σ a, β a)), a ∈ l.map sigma.fst →
id                                          └──┘           └──┘ └───────┘
src                                           └──┘                └──┘ └───────┘
typ                                         └──┘           └──┘ └───────┘
282    ∃ (u w : list Σ a, β a) b, l = u ++ [⟨a, b⟩] ++ w ∧ erase_aux a l = u ++ [] ++ w
id             └──┘          └┘      └┘   └───────┘     └┘ └┘ └┘ 
src            └──┘                └┘        └┘    └───────┘        └┘ └┘ └┘
typ            └──┘          └┘      └┘   └───────┘     └┘ └┘ └┘ 
doc                                                        └───────┘
283  | []            := false.elim
id     └┘               └────────┘
src    └┘               └────────┘
typ    └┘               └────────┘
284  | (⟨a', b'⟩::t) := begin
id              └┘
src             └┘
typ             └┘
st                      └─────
285    by_cases e : a' = a,
id                  └┘  
src    └───────┘ └─┘  
typ    └───────┘ └─┘└┘
doc    └───────┘ └─┘   
txt    └───────┘ └─┘   
par    └───────┘ └─┘   
pid             └─┘   
st   ────────────────────┘└─
286    { subst a',
id             └┘
src      └────┘
typ      └────┘└┘
doc      └────┘
txt      └────┘
par      └────┘
pid           
st   ───┘└──────┘└─
287      simpa [erase_aux, and_comm] using show ∃ u w (x : β a),
id              └───────┘  └──────┘                          
src      └─────┘└───────┘└┘└──────┘└──────┘    └────────┘  
typ      └─────┘└───────┘└┘└──────┘└──────┘    └────────┘ 
doc      └─────┘└───────┘└┘        └──────┘     └────────┘   
txt      └─────┘         └┘        └──────┘     └────────┘   
par      └─────┘         └┘        └──────┘     └────────┘   
pid                    └┘        └────┘     └────────┘   
st   ────────────────────────────────────────────────────────────
288        t = u ++ w ∧ (sigma.mk a b') :: t = u ++ ⟨a, x⟩ :: w,
id               └┘      └──────┘                    
src  ─────┘   └┘   └──────┘   └┘         └┘ └┘   └─
typ  ─────┘   └┘   └──────┘   └┘        └┘ └┘   └─
doc  ─────┘                   └┘         └┘ └┘   └─
txt  ─────┘                   └┘         └┘ └┘   └─
par  ─────┘                   └┘         └┘ └┘   └─
pid  ─────┘                   └┘         └┘ └┘   └─
st   ────────────────────────────────────────────────────────────
289        from ⟨[], t, b', by simp⟩ },
id               └┘    └┘
src  ──────────┘ └┘└┘ └┘  └┘  └──┘└┘
typ  ──────────┘ └┘└┘└┘└┘└┘  └──┘└┘
doc  ──────────┘   └┘ └┘  └┘  └──┘└┘
txt  ──────────┘   └┘ └┘  └┘  └──┘└┘
par  ──────────┘   └┘ └┘  └┘  └──┘└┘
pid  ──────────┘   └┘ └┘  └┘  └────┘
st   ────────────────────────┘└───┘└┘└┘
290    { simp [erase_aux, e, ne.symm e],
id             └───────┘    └─────┘ 
src      └────┘└───────┘└┘ └┘└─────┘ 
typ      └────┘└───────┘└┘└┘└─────┘
doc      └────┘└───────┘└┘ └┘        
txt      └────┘         └┘ └┘        
par      └────┘         └┘ └┘        
pid                   └┘ └┘        
st   ─────────────────────────────────┘└─
291      suffices : ∀ (b : β a) (_ : sigma.mk a b ∈ t), ∃ u w (x : β a),
id                                                                  
src      └─────────┘ └────┘  └─────┘            └────────┘  
typ      └─────────┘ └────┘  └─────┘            └────────┘ 
doc      └─────────┘ └────┘  └─────┘              └────────┘   
txt      └─────────┘ └────┘  └─────┘              └────────┘   
par      └─────────┘ └────┘  └─────┘              └────────┘   
pid      └───────┘└┘ └────┘  └─────┘              └────────┘   
st   ────────────────────────────────────────────────────────────────────
292        (sigma.mk a' b') :: t = u ++ ⟨a, x⟩ :: w ∧
src  ─────┘             └┘         └┘ └┘    
typ  ─────┘             └┘         └┘ └┘    
doc  ─────┘             └┘         └┘ └┘    
txt  ─────┘             └┘         └┘ └┘    
par  ─────┘             └┘         └┘ └┘    
pid  ─────┘             └┘         └┘ └┘    
st   ─────────────────────────────────────────────────
293        (sigma.mk a' b') :: (erase_aux a t) = u ++ w,
id          └──────┘ └┘ └┘      └───────┘  
src  ─────┘ └──────┘    └┘   └───────┘  └┘    
typ  ─────┘ └──────┘└┘└┘└┘   └───────┘└┘    
doc  ─────┘             └┘   └───────┘  └┘    
txt  ─────┘             └┘              └┘    
par  ─────┘             └┘              └┘    
pid  ─────┘             └┘              └┘    
st   ─────────────────────────────────────────────────┘└─
294      { simpa [replace_aux, ne.symm e, e] },
id                └─────────┘  └─────┘   
src        └─────┘└─────────┘└┘└─────┘ └┘ └┘
typ        └─────┘└─────────┘└┘└─────┘└┘└┘
doc        └─────┘└─────────┘└┘        └┘ └┘
txt        └─────┘           └┘        └┘ └┘
par        └─────┘           └┘        └┘ └┘
pid                        └┘        └┘ 
st   ─────┘└────────────────────────────────┘└┘
295      intros b m,
src      └────────┘
typ      └────────┘
doc      └────────┘
txt      └────────┘
par      └────────┘
pid            └──┘
st   ─────────────┘└─
296      have IH : ∀ (x : β a) (_ : sigma.mk a x ∈ t), ∃ u w (x : β a),
id                                  └──────┘                        
src      └────────┘ └────┘  └─────┘└──────┘     └────────┘  
typ      └────────┘ └────┘  └─────┘└──────┘     └────────┘ 
doc      └────────┘ └────┘  └─────┘              └────────┘   
txt      └────────┘ └────┘  └─────┘              └────────┘   
par      └────────┘ └────┘  └─────┘              └────────┘   
pid      └─────┘└─┘ └────┘  └─────┘              └────────┘   
st   ───────────────────────────────────────────────────────────────────
297        t = u ++ ⟨a, x⟩ :: w ∧ erase_aux a t = u ++ w,
id                                └───────┘  
src  ─────┘       └┘ └┘    └───────┘      
typ  ─────┘       └┘ └┘    └───────┘    
doc  ─────┘       └┘ └┘    └───────┘      
txt  ─────┘       └┘ └┘                   
par  ─────┘       └┘ └┘                   
pid  ─────┘       └┘ └┘                   
st   ──────────────────────────────────────────────────┘└─
298      { simpa using valid.erase_aux t },
id                     └─────────────┘ 
src        └──────────┘                
typ        └──────────┘└─────────────┘
doc        └──────────┘                
txt        └──────────┘                
par        └──────────┘                
pid             └────┘                
st   ─────┘└────────────────────────────┘└┘
299      rcases IH b m with ⟨u, w, b'', hl, hfl⟩,
id              └┘  
src      └─────┘    └────────────────────────┘
typ      └─────┘└┘└────────────────────────┘
doc      └─────┘    └────────────────────────┘
txt      └─────┘    └────────────────────────┘
par      └─────┘    └────────────────────────┘
pid                └────────────────────────┘
st   ──────────────────────────────────────────┘└─
300      exact ⟨⟨a', b'⟩ :: u, w, b'', by simp [hl, hfl.symm]⟩ }
id               └┘  └┘         └─┘           └┘
src      └────┘    └┘  └┘   └┘ └┘   └┘  └────┘  └┘        └┘
typ      └────┘  └┘└┘└┘└┘  └┘└┘└─┘└┘  └────┘└┘└┘└──────┘└┘
doc      └────┘    └┘  └┘   └┘ └┘   └┘  └────┘  └┘        └┘
txt      └────┘    └┘  └┘   └┘ └┘   └┘  └────┘  └┘        └┘
par      └────┘    └┘  └┘   └┘ └┘   └┘  └────┘  └┘        └┘
pid               └┘  └┘   └┘ └┘   └┘  └─────┘  └┘        └┘
st   ───────────────────────────────────┘└──────────────────┘└┘└─
301  end
st   ──┘
302  
303  theorem valid.erase {n} {bkts : bucket_array α β n} {sz}
id                                   └──────────┘   
src                                  └──────────┘
typ                                  └──────────┘   
doc                                  └──────────┘
304    (a : α) (Hc : contains_aux a (bkts.read hash_fn a))
id                  └──────────┘   └──┘└───┘ └─────┘ 
src                  └──────────┘        └───┘
typ                 └──────────┘   └──┘└───┘ └─────┘ 
doc                  └──────────┘        └───┘
305    (v : valid bkts sz) : valid (bkts.modify hash_fn a (erase_aux a)) (sz-1) :=
id          └───┘ └──┘ └┘    └───┘  └──┘└─────┘ └─────┘   └───────┘     └┘
src         └───┘            └───┘      └─────┘            └───────┘        
typ         └───┘ └──┘ └┘    └───┘  └──┘└─────┘ └─────┘   └───────┘     └┘
doc         └───┘            └───┘      └─────┘            └───────┘
306  begin
st   └─────
307    have nd := v.nodup (mk_idx n (hash_fn a)),
id                └─────┘  └────┘   └─────┘ 
src    └─────────┘└─────┘ └────┘          └┘
typ    └─────────┘└─────┘ └────┘ └─────┘└┘
doc    └─────────┘        └────┘          └┘
txt    └─────────┘                        └┘
par    └─────────┘                        └┘
pid    └─────┘└─┘                        └┘
st   ──────────────────────────────────────────┘└─
308    rcases hash_map.valid.erase_aux a (array.read bkts (mk_idx n (hash_fn a)))
id                                        └────────┘ └──┘  └────┘   └─────┘ 
src    └─────┘                          └────────┘     └────┘          └───
typ    └─────┘                          └────────┘└──┘ └────┘ └─────┘└───
doc    └─────┘                                         └────┘          └───
txt    └─────┘                                                         └───
par    └─────┘                                                         └───
pid                                                                   └───
st   ─────────────────────────────────────────────────────────────────────────────
309      ((contains_aux_iff nd).1 Hc) with ⟨u, w, b, hl, hfl⟩,
id         └──────────────┘ └┘    └┘
src  ───┘  └──────────────┘  └──┘  └───────────────────────┘
typ  ───┘  └──────────────┘└┘└──┘└┘└───────────────────────┘
doc  ───┘                    └──┘  └───────────────────────┘
txt  ───┘                    └──┘  └───────────────────────┘
par  ───┘                    └──┘  └───────────────────────┘
pid  ───┘                    └──┘  └───────────────────────┘
st   ───────────────────────────────────────────────────────┘└─
310    refine (v.modify hash_fn u [⟨a, b⟩] [] w hl hfl list.nodup_nil _ _ _).2;
id             └──────┘ └─────┘             └┘ └─┘ └────────────┘
src    └─────┘ └──────┘           └┘          └────────────┘└───────┘
typ    └─────┘ └──────┘└─────┘  └┘   └┘└─┘└────────────┘└───────┘
doc    └─────┘                    └┘                        └───────┘
txt    └─────┘                    └┘                        └───────┘
par    └─────┘                    └┘                        └───────┘
pid                              └┘                        └─────┘└┘
st   ───────────────────────────────────────────────────────────────────────────
311    { intros, simp at *; contradiction }
src      └────┘  └───────┘  └────────────┘
typ      └────┘  └───────┘  └────────────┘
doc      └────┘  └───────┘  └────────────┘
txt      └────┘  └───────┘  └────────────┘
par      └────┘  └───────┘  └────────────┘
pid                  └──┘               
st   ─┘└──────┘└─────────────────────────┘└─
312  end
st   ──┘
313  
314  end
315  end hash_map
316  
317  /-- A hash map data structure, representing a finite key-value map
318    with key type `α` and value type `β` (which may depend on `α`). -/
319  structure hash_map (α : Type u) [decidable_eq α] (β : α → Type v) :=
id                           └──┘     └──────────┘         
src                                   └──────────┘
typ                          └──┘     └──────────┘         
320  (hash_fn : α → nat)
id                └─┘
src                 └─┘
typ               └─┘
321  (size : ℕ)
id           
src          
typ          
322  (nbuckets : ℕ+)
id               └┘
src              └┘
typ              └┘
doc              └┘
323  (buckets : bucket_array α β nbuckets)
id              └──────────┘   └──────┘
src             └──────────┘
typ             └──────────┘   └──────┘
doc             └──────────┘
324  (is_valid : hash_map.valid hash_fn buckets size)
id               └────────────┘ └─────┘ └─────┘ └──┘
src              └────────────┘
typ              └────────────┘ └─────┘ └─────┘ └──┘
doc              └────────────┘
325  
326  /-- Construct an empty hash map with buffer size `nbuckets` (default 8). -/
327  def mk_hash_map {α : Type u} [decidable_eq α] {β : α → Type v} (hash_fn : α → nat) (nbuckets := 8) : hash_map α β :=
id                                 └──────────┘                                 └─┘                   └──────┘  
src                                └──────────┘                                    └─┘                   └──────┘
typ                                └──────────┘                                 └─┘                   └──────┘  
doc                                                                                                      └──────┘
328  let n := if nbuckets = 0 then 8 else nbuckets in
id              └──────┘                └──────┘
src                       
typ             └──────┘                └──────┘
329  let nz : n > 0 := by abstract { cases nbuckets; simp [if_pos, nat.succ_ne_zero] } in
id                                       └──────┘        └────┘  └──────────────┘
src                      └─────────┘└────┘        └┘└────┘└────┘└┘└──────────────┘└┘└┘
typ                     └─────────┘└────┘└──────┘└┘└────┘└────┘└┘└──────────────┘└┘└┘
doc                       └─────────┘└────┘        └┘└────┘      └┘                └┘└┘
txt                       └─────────┘└────┘        └┘└────┘      └┘                └┘└┘
par                       └─────────┘└────┘        └┘└────┘      └┘                └┘└┘
pid                               └──────┘        └──────┘      └┘                └─┘
st                       └─────────┘└───────────────────────────────────────────────┘
330  { hash_fn  := hash_fn,
id                 └─────┘
typ                └─────┘
331    size     := 0,
332    nbuckets := ⟨n, nz⟩,
id                    └┘
typ                   └┘
333    buckets  := mk_array n [],
id                 └──────┘  └┘
src                └──────┘   └┘
typ                └──────┘  └┘
334    is_valid := hash_map.mk_valid _ _ }
id                 └───────────────┘
src                └───────────────┘
typ                └───────────────┘
335  
336  namespace hash_map
337  variables {α : Type u} {β : α → Type v} [decidable_eq α]
id                                           └──────────┘
src                                           └──────────┘
typ                                          └──────────┘
338  
339  /-- Return the value corresponding to a key, or `none` if not found -/
340  def find (m : hash_map α β) (a : α) : option (β a) :=
id                 └──────┘             └────┘   
src                └──────┘                └────┘
typ                └──────┘             └────┘   
doc                └──────┘
341  find_aux a (m.buckets.read m.hash_fn a)
id   └──────┘   └──────┘└───┘ └──────┘ 
src  └──────┘     └──────┘└───┘  └──────┘
typ  └──────┘   └──────┘└───┘ └──────┘ 
doc  └──────┘             └───┘
342  
343  /-- Return `tt` if the key exists in the map -/
344  def contains (m : hash_map α β) (a : α) : bool :=
id                     └──────┘             └──┘
src                    └──────┘                └──┘
typ                    └──────┘             └──┘
doc                    └──────┘
345  (m.find a).is_some
id    └───┘  └─────┘
src    └───┘   └─────┘
typ   └───┘  └─────┘
doc    └───┘
346  
347  instance : has_mem α (hash_map α β) := ⟨λa m, m.contains a⟩
id              └─────┘   └──────┘            └───────┘ 
src             └─────┘    └──────┘                 └───────┘
typ             └─────┘   └──────┘            └───────┘ 
doc                        └──────┘                 └───────┘
348  
349  /-- Fold a function over the key-value pairs in the map -/
350  def fold {δ : Type w} (m : hash_map α β) (d : δ) (f : δ → Π a, β a → δ) : δ :=
id                              └──────┘                               
src                             └──────┘
typ                             └──────┘                               
doc                             └──────┘
351  m.buckets.foldl d f
id   └──────┘└────┘  
src   └──────┘└────┘
typ  └──────┘└────┘  
doc           └────┘
352  
353  /-- The list of key-value pairs in the map -/
354  def entries (m : hash_map α β) : list Σ a, β a :=
id                    └──────┘      └──┘    
src                   └──────┘        └──┘   
typ                   └──────┘      └──┘    
doc                   └──────┘
355  m.buckets.as_list
id   └──────┘└──────┘
src   └──────┘└──────┘
typ  └──────┘└──────┘
doc           └──────┘
356  
357  /-- The list of keys in the map -/
358  def keys (m : hash_map α β) : list α :=
id                 └──────┘      └──┘ 
src                └──────┘        └──┘
typ                └──────┘      └──┘ 
doc                └──────┘
359  m.entries.map sigma.fst
id   └──────┘└──┘ └───────┘
src   └──────┘└──┘ └───────┘
typ  └──────┘└──┘ └───────┘
doc   └──────┘
360  
361  theorem find_iff (m : hash_map α β) (a : α) (b : β a) :
id                         └──────┘                 
src                        └──────┘
typ                        └──────┘                 
doc                        └──────┘
362    m.find a = some b ↔ sigma.mk a b ∈ m.entries :=
id     └───┘   └──┘   └──────┘    └──────┘
src     └───┘    └──┘    └──────┘       └──────┘
typ    └───┘   └──┘   └──────┘    └──────┘
doc     └───┘                              └──────┘
363  m.is_valid.find_aux_iff _
id   └───────┘└───────────┘
src   └───────┘└───────────┘
typ  └───────┘└───────────┘
364  
365  theorem contains_iff (m : hash_map α β) (a : α) :
id                             └──────┘         
src                            └──────┘
typ                            └──────┘         
doc                            └──────┘
366    m.contains a ↔ a ∈ m.keys :=
id     └───────┘     └───┘
src     └───────┘        └───┘
typ    └───────┘     └───┘
doc     └───────┘          └───┘
367  m.is_valid.contains_aux_iff _ _
id   └───────┘└───────────────┘
src   └───────┘└───────────────┘
typ  └───────┘└───────────────┘
368  
369  theorem entries_empty (hash_fn : α → nat) (n) :
id                                       └─┘
src                                       └─┘
typ                                      └─┘
370    (@mk_hash_map α _ β hash_fn n).entries = [] :=
id       └─────────┘     └─────┘  └─────┘   └┘
src      └─────────┘                 └─────┘   └┘
typ      └─────────┘     └─────┘  └─────┘   └┘
doc      └─────────┘                 └─────┘
371  by dsimp [entries, mk_hash_map]; rw mk_as_list
id             └─────┘  └─────────┘      └────────┘
src     └─────┘└─────┘└┘└─────────┘  └─┘└────────┘
typ     └─────┘└─────┘└┘└─────────┘  └─┘└────────┘
doc     └─────┘└─────┘└┘└─────────┘  └─┘          
txt     └─────┘       └┘             └─┘          
par     └─────┘       └┘             └─┘          
pid                 └┘                         
st     └────────────────────────────────┘└────────┘
372  
src  
typ  
doc  
txt  
par  
pid  
st   
373  theorem keys_empty (hash_fn : α → nat) (n) :
id                                    └─┘
src                                    └─┘
typ                                   └─┘
374    (@mk_hash_map α _ β hash_fn n).keys = [] :=
id       └─────────┘     └─────┘  └──┘   └┘
src      └─────────┘                 └──┘   └┘
typ      └─────────┘     └─────┘  └──┘   └┘
doc      └─────────┘                 └──┘
375  by dsimp [keys]; rw entries_empty; refl
id             └──┘      └───────────┘
src     └─────┘└──┘  └─┘└───────────┘  └────
typ     └─────┘└──┘  └─┘└───────────┘  └────
doc     └─────┘└──┘  └─┘               └────
txt     └─────┘      └─┘               └────
par     └─────┘      └─┘               └────
pid                                     
st     └────────────────┘└───────────┘└──────
376  
src  
typ  
doc  
txt  
par  
pid  
st   
377  theorem find_empty (hash_fn : α → nat) (n a) :
id                                    └─┘
src                                    └─┘
typ                                   └─┘
378    (@mk_hash_map α _ β hash_fn n).find a = none :=
id       └─────────┘     └─────┘  └──┘    └──┘
src      └─────────┘                 └──┘     └──┘
typ      └─────────┘     └─────┘  └──┘    └──┘
doc      └─────────┘                 └──┘
379  by induction h : (@mk_hash_map α _ β hash_fn n).find a; [refl,
id                      └─────────┘     └─────┘          
src     └────────┘ └─┘  └─────────┘ └─┘         └─────┘   └──┘
typ     └────────┘ └─┘  └─────────┘└─┘└─────┘└─────┘  └──┘
doc     └────────┘ └─┘  └─────────┘ └─┘         └─────┘    └──┘
txt     └────────┘ └─┘              └─┘         └─────┘    └──┘
par     └────────┘ └─┘              └─┘         └─────┘    └──┘
pid               └─┘              └─┘         └─────┘
st     └────────────────────────────────────────────────────────────
380     { have := (find_iff _ _ _).1 h, rw entries_empty at this, contradiction }]
id                 └──────┘               └───────────┘
src       └──────┘ └──────┘└────────┘   └─┘└───────────┘└──────┘  └────────────┘
typ       └──────┘ └──────┘└────────┘  └─┘└───────────┘└──────┘  └────────────┘
doc       └──────┘         └────────┘   └─┘             └──────┘  └────────────┘
txt       └──────┘         └────────┘   └─┘             └──────┘  └────────────┘
par       └──────┘         └────────┘   └─┘             └──────┘  └────────────┘
pid       └───┘└─┘         └────────┘                  └──────┘               
st   ──┘└────────────────────────────┘└────────────────────────┘└──────────────┘└┘
381  
382  theorem not_contains_empty (hash_fn : α → nat) (n a) :
id                                            └─┘
src                                            └─┘
typ                                           └─┘
383    ¬ (@mk_hash_map α _ β hash_fn n).contains a :=
id        └─────────┘     └─────┘  └──────┘  
src       └─────────┘                 └──────┘
typ       └─────────┘     └─────┘  └──────┘  
doc        └─────────┘                 └──────┘
384  by apply bool_iff_false.2; dsimp [contains]; rw [find_empty]; refl
id            └────────────┘           └──────┘       └────────┘
src     └────┘└────────────┘└┘  └─────┘└──────┘  └──┘└────────┘  └────
typ     └────┘└────────────┘└┘  └─────┘└──────┘  └──┘└────────┘  └────
doc     └────┘              └┘  └─────┘└──────┘  └──┘            └────
txt     └────┘              └┘  └─────┘          └──┘            └────
par     └────┘              └┘  └─────┘          └──┘            └────
pid                        └┘                   └┘                
st     └─────────────────────────────────────────────┘└────────┘└──────
385  
src  
typ  
doc  
txt  
par  
pid  
st   
386  theorem insert_lemma (hash_fn : α → nat) {n n'}
id                                      └─┘
src                                      └─┘
typ                                     └─┘
387    {bkts : bucket_array α β n} {sz} (v : valid hash_fn bkts sz) :
id             └──────────┘               └───┘ └─────┘ └──┘ └┘
src            └──────────┘                  └───┘
typ            └──────────┘               └───┘ └─────┘ └──┘ └┘
doc            └──────────┘                  └───┘
388    valid hash_fn (bkts.foldl (mk_array _ [] : bucket_array α β n') (reinsert_aux hash_fn)) sz :=
id     └───┘ └─────┘  └──┘└────┘  └──────┘   └┘   └──────────┘   └┘   └──────────┘ └─────┘   └┘
src    └───┘              └────┘  └──────┘   └┘   └──────────┘          └──────────┘
typ    └───┘ └─────┘  └──┘└────┘  └──────┘   └┘   └──────────┘   └┘   └──────────┘ └─────┘   └┘
doc    └───┘              └────┘                  └──────────┘          └──────────┘
389  begin
st   └─────
390    suffices : ∀ (l : list Σ a, β a) (t : bucket_array α β n') sz,
id                       └──┘               └──────────┘    └┘
src    └─────────┘ └────┘└──┘ └┘   └─────┘└──────────┘    └──┘ 
typ    └─────────┘ └────┘└──┘ └┘  └─────┘└──────────┘ └┘└──┘ 
doc    └─────────┘ └────┘     └┘   └─────┘└──────────┘    └──┘ 
txt    └─────────┘ └────┘     └┘   └─────┘                └──┘ 
par    └─────────┘ └────┘     └┘   └─────┘                └──┘ 
pid    └───────┘└┘ └────┘     └┘   └─────┘                └──┘ 
st   ─────────────────────────────────────────────────────────────────
391      valid hash_fn t sz → ((l ++ t.as_list).map sigma.fst).nodup →
id       └───┘                    └┘  └──────┘      └───────┘
src  ───┘                   └┘ └──────┘└────┘└───────┘└──────┘ 
typ  ───┘└───┘              └┘ └──────┘└────┘└───────┘└──────┘ 
doc  ───┘                      └──────┘└────┘         └──────┘ 
txt  ───┘                              └────┘         └──────┘ 
par  ───┘                              └────┘         └──────┘ 
pid  ───┘                              └────┘         └──────┘ 
st   ──────────────────────────────────────────────────────────────────
392      valid hash_fn (l.foldl (λr (a : Σ a, β a), reinsert_aux hash_fn r a.1 a.2) t) (sz + l.length),
id       └───┘           └────┘                  └──────────┘ └─────┘                     └─────┘
src  ───┘└───┘         └────┘  └─────┘└┘  └─┘└──────────┘         └─┘ └──┘ └┘    └─────┘
typ  ───┘└───┘         └────┘  └─────┘└┘ └─┘└──────────┘└─────┘  └─┘ └──┘ └┘    └─────┘
doc  ───┘└───┘                 └─────┘ └┘   └─┘└──────────┘         └─┘ └──┘ └┘            
txt  ───┘                      └─────┘ └┘   └─┘                     └─┘ └──┘ └┘            
par  ───┘                      └─────┘ └┘   └─┘                     └─┘ └──┘ └┘            
pid  ───┘                      └─────┘ └┘   └─┘                     └─┘ └──┘ └┘            
st   ────────────────────────────────────────────────────────────────────────────────────────────────┘└─
393    { have p := this bkts.as_list _ _ (mk_valid _ _),
id                 └──┘ └──────────┘      └──────┘
src      └────────┘    └──────────┘└───┘ └──────┘└───┘
typ      └────────┘└──┘└──────────┘└───┘ └──────┘└───┘
doc      └────────┘    └──────────┘└───┘         └───┘
txt      └────────┘                └───┘         └───┘
par      └────────┘                └───┘         └───┘
pid      └────┘└─┘                └───┘         └───┘
st   ───┘└────────────────────────────────────────────┘└─
394      rw [mk_as_list, list.append_nil, zero_add, v.len] at p,
id           └────────┘  └─────────────┘  └──────┘
src      └──┘└────────┘└┘└─────────────┘└┘└──────┘└┘     └────┘
typ      └──┘└────────┘└┘└─────────────┘└┘└──────┘└┘└───┘└────┘
doc      └──┘          └┘               └┘        └┘     └────┘
txt      └──┘          └┘               └┘        └┘     └────┘
par      └──┘          └┘               └┘        └┘     └────┘
pid        └┘          └┘               └┘        └┘     └───┘
st   ─────────────────┘└───────────────┘└────────┘└─────┘└───┘└─
395      rw bucket_array.foldl_eq,
id          └───────────────────┘
src      └─┘└───────────────────┘
typ      └─┘└───────────────────┘
doc      └─┘
txt      └─┘
par      └─┘
pid        
st   ───────────────────────────┘└─
396      exact p (v.as_list_nodup _) },
id               └─────────────┘
src      └────┘  └─────────────┘└──┘
typ      └────┘ └─────────────┘└──┘
doc      └────┘                 └──┘
txt      └────┘                 └──┘
par      └────┘                 └──┘
pid                            └─┘
st   ───────────────────────────────┘└┘
397    intro l, induction l with c l IH; intros t sz v nd, {exact v},
id                                                               
src    └─────┘  └────────┘ └──────────┘  └──────────────┘   └────┘
typ    └─────┘  └────────┘└──────────┘  └──────────────┘   └────┘
doc    └─────┘  └────────┘ └──────────┘  └──────────────┘   └────┘
txt    └─────┘  └────────┘ └──────────┘  └──────────────┘   └────┘
par    └─────┘  └────────┘ └──────────┘  └──────────────┘   └────┘
pid         └┘            └─────────┘        └────────┘        
st   ────────┘└─────────────────────────────────────────┘└────────┘└┘
398    rw show sz + (c :: l).length = sz + 1 + l.length, by simp,
id                                  └┘       └──────┘
src    └─┘            └───────┘   └─┘ └──────┘└───┘└──┘
typ    └─┘           └───────┘└┘ └─┘ └──────┘└───┘└──┘
doc    └─┘            └───────┘    └─┘         └───┘└──┘
txt    └─┘            └───────┘    └─┘         └───┘└──┘
par    └─┘            └───────┘    └─┘         └───┘└──┘
pid                  └───────┘    └─┘         └───────┘
st   ─────────────────────────────────────────────────────┘└───┘└─
399    rcases (show (l.map sigma.fst).nodup ∧
id                                          
src    └─────┘                    └──────┘
typ    └─────┘                    └──────┘
doc    └─────┘                    └──────┘ 
txt    └─────┘                    └──────┘ 
par    └─────┘                    └──────┘ 
pid                              └──────┘ 
st   ─────────────────────────────────────────
400        ((bucket_array.as_list t).map sigma.fst).nodup ∧
src  ─────┘                       └────┘         └──────┘ 
typ  ─────┘                       └────┘         └──────┘ 
doc  ─────┘                       └────┘         └──────┘ 
txt  ─────┘                       └────┘         └──────┘ 
par  ─────┘                       └────┘         └──────┘ 
pid  ─────┘                       └────┘         └──────┘ 
st   ───────────────────────────────────────────────────────
401        c.fst ∉ l.map sigma.fst ∧
id               
src  ─────┘                    
typ  ─────┘                    
doc  ─────┘                     
txt  ─────┘                     
par  ─────┘                     
pid  ─────┘                     
st   ────────────────────────────────
402        c.fst ∉ (bucket_array.as_list t).map sigma.fst ∧
id         └───┘
src  ─────┘└───┘                       └────┘          
typ  ─────┘└───┘                       └────┘          
doc  ─────┘                            └────┘          
txt  ─────┘                            └────┘          
par  ─────┘                            └────┘          
pid  ─────┘                            └────┘          
st   ───────────────────────────────────────────────────────
403        (l.map sigma.fst).disjoint ((bucket_array.as_list t).map sigma.fst),
id          └───┘                       └──────────────────┘       └───────┘
src  ─────┘ └───┘         └─────────┘  └──────────────────┘ └────┘└───────┘└──
typ  ─────┘ └───┘         └─────────┘  └──────────────────┘└────┘└───────┘└──
doc  ─────┘               └─────────┘  └──────────────────┘ └────┘         └──
txt  ─────┘               └─────────┘                       └────┘         └──
par  ─────┘               └─────────┘                       └────┘         └──
pid  ─────┘               └─────────┘                       └────┘         └──
st   ───────────────────────────────────────────────────────────────────────────
404      by simpa [list.nodup_append, not_or_distrib, and_comm, and.left_comm] using nd)
id                 └───────────────┘  └────────────┘  └──────┘  └───────────┘        └┘
src  ──────┘└─────┘└───────────────┘└┘└────────────┘└┘└──────┘└┘└───────────┘└──────┘  └─
typ  ──────┘└─────┘└───────────────┘└┘└────────────┘└┘└──────┘└┘└───────────┘└──────┘└┘└─
doc  ──────┘└─────┘                 └┘              └┘        └┘             └──────┘  └─
txt  ──────┘└─────┘                 └┘              └┘        └┘             └──────┘  └─
par  ──────┘└─────┘                 └┘              └┘        └┘             └──────┘  └─
pid  ─────────────┘                 └┘              └┘        └┘             └──────┘  └─
st   ─────┘└──────────────────────────────────────────────────────────────────────────┘└─
405      with ⟨nd1, nd2, nm1, nm2, dj⟩,
src  ────────────────────────────────┘
typ  ────────────────────────────────┘
doc  ────────────────────────────────┘
txt  ────────────────────────────────┘
par  ────────────────────────────────┘
pid  ────────────────────────────────┘
st   ────────────────────────────────┘└─
406    have v' := v.insert _ _ c.2 (λHc, nm2 $ (v.contains_aux_iff _ c.1).1 Hc),
id                └──────┘               └─┘    └────────────────┘   
src    └─────────┘└──────┘└───┘ └─┘  └──┘     └────────────────┘└─┘ └────┘  
typ    └─────────┘└──────┘└───┘ └─┘  └──┘└─┘  └────────────────┘└─┘└────┘  
doc    └─────────┘        └───┘ └─┘  └──┘                       └─┘ └────┘  
txt    └─────────┘        └───┘ └─┘  └──┘                       └─┘ └────┘  
par    └─────────┘        └───┘ └─┘  └──┘                       └─┘ └────┘  
pid    └─────┘└─┘        └───┘ └─┘  └──┘                       └─┘ └────┘  
st   ─────────────────────────────────────────────────────────────────────────┘└─
407    apply IH _ _ v',
id           └┘     └┘
src    └────┘  └───┘
typ    └────┘└┘└───┘└┘
doc    └────┘  └───┘
txt    └────┘  └───┘
par    └────┘  └───┘
pid           └───┘
st   ────────────────┘└─
408    suffices : ∀ ⦃a : α⦄ (b : β a), sigma.mk a b ∈ l →
id                                                  
src    └─────────┘ └────┘ └─────┘                
typ    └─────────┘ └────┘└─────┘              
doc    └─────────┘ └────┘ └─────┘                
txt    └─────────┘ └────┘ └─────┘                
par    └─────────┘ └────┘ └─────┘                
pid    └───────┘└┘ └────┘ └─────┘                
st   ─────────────────────────────────────────────────────
409      ∀ (b' : β a), sigma.mk a b' ∈ (reinsert_aux hash_fn t c.1 c.2).as_list → false,
id                    └──────┘        └──────────┘ └─────┘                    └───┘
src  ───┘ └─────┘   └──────┘     └──────────┘         └─┘ └──────────┘ └───┘
typ  ───┘ └─────┘  └──────┘    └──────────┘└─────┘ └─┘└──────────┘ └───┘
doc  ───┘ └─────┘                └──────────┘         └─┘ └──────────┘ 
txt  ───┘ └─────┘                                     └─┘ └──────────┘ 
par  ───┘ └─────┘                                     └─┘ └──────────┘ 
pid  ───┘ └─────┘                                     └─┘ └──────────┘ 
st   ─────────────────────────────────────────────────────────────────────────────────┘└─
410    { simpa [list.nodup_append, nd1, v'.as_list_nodup _, list.disjoint] },
id              └───────────────┘  └─┘  └──────────────┘    └───────────┘
src      └─────┘└───────────────┘└┘   └┘└──────────────┘└──┘└───────────┘└┘
typ      └─────┘└───────────────┘└┘└─┘└┘└──────────────┘└──┘└───────────┘└┘
doc      └─────┘                 └┘   └┘                └──┘└───────────┘└┘
txt      └─────┘                 └┘   └┘                └──┘             └┘
par      └─────┘                 └┘   └┘                └──┘             └┘
pid                            └┘   └┘                └──┘             
st   ───┘└────────────────────────────────────────────────────────────────┘└┘
411    intros a b m1 b' m2,
src    └─────────────────┘
typ    └─────────────────┘
doc    └─────────────────┘
txt    └─────────────────┘
par    └─────────────────┘
pid          └───────────┘
st   ────────────────────┘└─
412    rcases (reinsert_aux hash_fn t c.1 c.2).mem_as_list.1 m2 with ⟨i, im⟩,
id             └──────────┘ └─────┘                        └┘
src    └─────┘ └──────────┘         └─┘ └────────────────┘  └───────────┘
typ    └─────┘ └──────────┘└─────┘ └─┘└────────────────┘└┘└───────────┘
doc    └─────┘ └──────────┘         └─┘ └────────────────┘  └───────────┘
txt    └─────┘                      └─┘ └────────────────┘  └───────────┘
par    └─────┘                      └─┘ └────────────────┘  └───────────┘
pid                                └─┘ └────────────────┘  └───────────┘
st   ──────────────────────────────────────────────────────────────────────┘└─
413    have : sigma.mk a b' ∉ array.read t i,
id            └──────┘  └┘   └────────┘  
src    └─────┘└──────┘    └────────┘ 
typ    └─────┘└──────┘└┘ └────────┘
doc    └─────┘                       
txt    └─────┘                       
par    └─────┘                       
pid    └───┘└┘                       
st   ──────────────────────────────────────┘└─
414    { intro m3,
src      └──────┘
typ      └──────┘
doc      └──────┘
txt      └──────┘
par      └──────┘
pid           └─┘
st   ───┘└──────┘└─
415      have : a ∈ list.map sigma.fst t.as_list :=
id                 └──────┘ └───────┘ └───────┘
src      └─────┘  └──────┘└───────┘└───────┘└───
typ      └─────┘ └──────┘└───────┘└───────┘└───
doc      └─────┘                   └───────┘└───
txt      └─────┘                            └───
par      └─────┘                            └───
pid      └───┘└┘                            └───
st   ───────────────────────────────────────────────
416        list.mem_map_of_mem sigma.fst (t.mem_as_list.2 ⟨_, m3⟩),
id         └─────────────────┘ └───────┘  └───────────┘       └┘
src  ─────┘└─────────────────┘└───────┘ └───────────┘└─┘ └─┘  └┘
typ  ─────┘└─────────────────┘└───────┘ └───────────┘└─┘ └─┘└┘└┘
doc  ─────┘                                          └─┘ └─┘  └┘
txt  ─────┘                                          └─┘ └─┘  └┘
par  ─────┘                                          └─┘ └─┘  └┘
pid  ─────┘                                          └─┘ └─┘  └┘
st   ────────────────────────────────────────────────────────────┘└─
417      exact dj (list.mem_map_of_mem sigma.fst m1) this },
id             └┘  └─────────────────┘ └───────┘ └┘  └──┘
src      └────┘   └─────────────────┘└───────┘  └┘    
typ      └────┘└┘ └─────────────────┘└───────┘└┘└┘└──┘
doc      └────┘                                 └┘    
txt      └────┘                                 └┘    
par      └────┘                                 └┘    
pid                                            └┘    
st   ────────────────────────────────────────────────────┘└┘
418    by_cases h : mk_idx n' (hash_fn c.1) = i,
id                  └────┘ └┘  └─────┘       
src    └───────┘ └─┘└────┘           └──┘ 
typ    └───────┘ └─┘└────┘└┘ └─────┘└──┘ 
doc    └───────┘ └─┘└────┘           └──┘ 
txt    └───────┘ └─┘                 └──┘ 
par    └───────┘ └─┘                 └──┘ 
pid             └─┘                 └──┘ 
st   ─────────────────────────────────────────┘└─
419    { subst h,
id             
src      └────┘
typ      └────┘
doc      └────┘
txt      └────┘
par      └────┘
pid           
st   ───┘└─────┘└─
420      have e : sigma.mk a b' = ⟨c.1, c.2⟩,
id                └──────┘  └┘         
src      └───────┘└──────┘      └──┘ └─┘
typ      └───────┘└──────┘└┘   └──┘└─┘
doc      └───────┘              └──┘ └─┘
txt      └───────┘              └──┘ └─┘
par      └───────┘              └──┘ └─┘
pid      └────┘└─┘              └──┘ └─┘
st   ──────────────────────────────────────┘└─
421      { simpa [reinsert_aux, bucket_array.modify, array.read_write, this] using im },
id                └──────────┘  └─────────────────┘  └──────────────┘  └──┘        └┘
src        └─────┘└──────────┘└┘└─────────────────┘└┘└──────────────┘└┘    └──────┘  
typ        └─────┘└──────────┘└┘└─────────────────┘└┘└──────────────┘└┘└──┘└──────┘└┘
doc        └─────┘└──────────┘└┘└─────────────────┘└┘                └┘    └──────┘  
txt        └─────┘            └┘                   └┘                └┘    └──────┘  
par        └─────┘            └┘                   └┘                └┘    └──────┘  
pid                         └┘                   └┘                └┘    └────┘  
st   ─────┘└─────────────────────────────────────────────────────────────────────────┘└┘
422      injection e with e, subst a,
id                                
src      └────────┘ └─────┘  └────┘
typ      └────────┘└─────┘  └────┘
doc      └────────┘ └─────┘  └────┘
txt      └────────┘ └─────┘  └────┘
par      └────────┘ └─────┘  └────┘
pid                └─────┘       
st   ─────────────────────┘└───────┘└─
423      exact nm1.elim (@list.mem_map_of_mem _ _ sigma.fst _ _ m1) },
id             └──────┘   └─────────────────┘     └───────┘     └┘
src      └────┘└──────┘  └─────────────────┘└───┘└───────┘└───┘  └┘
typ      └────┘└──────┘  └─────────────────┘└───┘└───────┘└───┘└┘└┘
doc      └────┘                             └───┘         └───┘  └┘
txt      └────┘                             └───┘         └───┘  └┘
par      └────┘                             └───┘         └───┘  └┘
pid                                        └───┘         └───┘  
st   ──────────────────────────────────────────────────────────────┘└┘
424    { apply this,
src      └────┘
typ      └────┘
doc      └────┘
txt      └────┘
par      └────┘
pid           
st   ─────────────┘└─
425      simpa [reinsert_aux, bucket_array.modify, array.read_write_of_ne _ _ h] using im }
id              └──────────┘  └─────────────────┘  └────────────────────┘             └┘
src      └─────┘└──────────┘└┘└─────────────────┘└┘└────────────────────┘└───┘ └──────┘  
typ      └─────┘└──────────┘└┘└─────────────────┘└┘└────────────────────┘└───┘└──────┘└┘
doc      └─────┘└──────────┘└┘└─────────────────┘└┘                      └───┘ └──────┘  
txt      └─────┘            └┘                   └┘                      └───┘ └──────┘  
par      └─────┘            └┘                   └┘                      └───┘ └──────┘  
pid                       └┘                   └┘                      └───┘ └────┘  
st   ────────────────────────────────────────────────────────────────────────────────────┘└─
426  end
st   ──┘
427  
428  /-- Insert a key-value pair into the map. (Modifies `m` in-place when applicable) -/
429  def insert : Π (m : hash_map α β) (a : α) (b : β a), hash_map α β
id                      └──────┘                    └──────┘  
src                     └──────┘                         └──────┘
typ                     └──────┘                    └──────┘  
doc                      └──────┘                         └──────┘
430  | ⟨hash_fn, size, n, buckets, v⟩ a b :=
id      └─────┘  └──┘    └─────┘     
typ     └─────┘  └──┘    └─────┘     
431  let bkt := buckets.read hash_fn a in
id       └─┘           └───┘
src                    └───┘
typ      └─┘           └───┘
doc                    └───┘
432  if hc : contains_aux a bkt then
id   └┘      └──────────┘   └─┘
src  └┘      └──────────┘
typ  └┘      └──────────┘   └─┘
doc          └──────────┘
433  { hash_fn  := hash_fn,
434    size     := size,
435    nbuckets := n,
436    buckets  := buckets.modify hash_fn a (replace_aux a b),
id                        └─────┘            └─────────┘
src                       └─────┘            └─────────┘
typ                       └─────┘            └─────────┘
doc                       └─────┘            └─────────┘
437    is_valid := v.replace _ a b hc }
id                  └──────┘       └┘
src                 └──────┘
typ                 └──────┘       └┘
438  else
439  let size'    := size + 1,
id   └─┘ └───┘            
src                       
typ  └─┘ └───┘            
440      buckets' := buckets.modify hash_fn a (λl, ⟨a, b⟩::l),
id       └──────┘           └─────┘                     └┘
src                         └─────┘                      └┘
typ      └──────┘           └─────┘                     └┘
doc                         └─────┘
441      valid'   := v.insert _ a b hc in
id       └────┘       └─────┘       └┘
src                   └─────┘
typ      └────┘       └─────┘       └┘
442  if size' ≤ n.1 then
id      └───┘   
src             
typ     └───┘   
443  { hash_fn  := hash_fn,
444    size     := size',
id                 └───┘
typ                └───┘
445    nbuckets := n,
446    buckets  := buckets',
id                 └──────┘
typ                └──────┘
447    is_valid := valid' }
id                 └────┘
typ                └────┘
448  else
449  let n'        : ℕ+ := ⟨n.1 * 2, mul_pos n.2 dec_trivial⟩,
id                   └┘            └─────┘    └─────────┘
src                  └┘            └─────┘    └─────────┘
typ                  └┘            └─────┘    └─────────┘
doc                  └┘                          └─────────┘
450      buckets'' : bucket_array α β n' :=
id                   └──────────┘   └┘
src                  └──────────┘
typ                  └──────────┘   └┘
doc                  └──────────┘
451                  buckets'.foldl (mk_array _ []) (reinsert_aux hash_fn) in
id                   └──────┘└────┘  └──────┘   └┘   └──────────┘
src                          └────┘  └──────┘   └┘   └──────────┘
typ                  └──────┘└────┘  └──────┘   └┘   └──────────┘
doc                          └────┘                  └──────────┘
452  { hash_fn  := hash_fn,
453    size     := size',
id                 └───┘
typ                └───┘
454    nbuckets := n',
id                 └┘
typ                └┘
455    buckets  := buckets'',
id                 └───────┘
typ                └───────┘
456    is_valid := insert_lemma _ valid' }
id                 └──────────┘   └────┘
src                └──────────┘
typ                └──────────┘   └────┘
457  
458  theorem mem_insert : Π (m : hash_map α β) (a b a' b'),
id                              └──────┘       └┘ └┘
src                              └──────┘
typ                             └──────┘       └┘ └┘
doc                              └──────┘
459    (sigma.mk a' b' : sigma β) ∈ (m.insert a b).entries ↔
id      └──────┘ └┘ └┘   └───┘     └─────┘   └─────┘  
src     └──────┘         └───┘       └─────┘     └─────┘  
typ     └──────┘ └┘ └┘   └───┘     └─────┘   └─────┘  
doc                                   └─────┘     └─────┘
460    if a = a' then b == b' else sigma.mk a' b' ∈ m.entries
id          └┘       └┘ └┘      └──────┘ └┘ └┘  └──────┘
src                    └┘         └──────┘         └──────┘
typ         └┘       └┘ └┘      └──────┘ └┘ └┘  └──────┘
doc                                                  └──────┘
461  | ⟨hash_fn, size, n, bkts, v⟩ a b a' b' := begin
st                                              └─────
462    let bkt := bkts.read hash_fn a,
id                └───────┘ └─────┘ 
src    └─────────┘└───────┘       
typ    └─────────┘└───────┘└─────┘
doc    └─────────┘└───────┘       
txt    └─────────┘                
par    └─────────┘                
pid    └─────┘└─┘                
st   ───────────────────────────────┘└─
463    have nd : (bkt.map sigma.fst).nodup := v.nodup (mk_idx n (hash_fn a)),
id                └─────┘ └───────┘           └─────┘  └────┘   └─────┘ 
src    └────────┘ └─────┘└───────┘└─────────┘└─────┘ └────┘          └┘
typ    └────────┘ └─────┘└───────┘└─────────┘└─────┘ └────┘ └─────┘└┘
doc    └────────┘                 └─────────┘        └────┘          └┘
txt    └────────┘                 └─────────┘                        └┘
par    └────────┘                 └─────────┘                        └┘
pid    └─────┘└─┘                 └────┘└───┘                        └┘
st   ──────────────────────────────────────────────────────────────────────┘└─
464    have lem : Π (bkts' : bucket_array α β n) (v1 u w)
id                           └──────────┘   
src    └─────────┘ └────────┘└──────────┘   └──────────
typ    └─────────┘ └────────┘└──────────┘└──────────
doc    └─────────┘ └────────┘└──────────┘   └──────────
txt    └─────────┘ └────────┘               └──────────
par    └─────────┘ └────────┘               └──────────
pid    └──────┘└─┘ └────────┘               └──────────
st   ─────────────────────────────────────────────────────
465      (hl : bucket_array.as_list bkts = u ++ v1 ++ w)
id                                          └┘
src  ─────────┘                         └┘     └─
typ  ─────────┘                         └┘     └─
doc  ─────────┘                                 └─
txt  ─────────┘                                 └─
par  ─────────┘                                 └─
pid  ─────────┘                                 └─
st   ────────────────────────────────────────────────────
466      (hfl : bucket_array.as_list bkts' = u ++ [⟨a, b⟩] ++ w)
id              └──────────────────┘       
src  ──────────┘└──────────────────┘            └┘     └─
typ  ──────────┘└──────────────────┘           └┘     └─
doc  ──────────┘└──────────────────┘            └┘     └─
txt  ──────────┘                                └┘     └─
par  ──────────┘                                └┘     └─
pid  ──────────┘                                └┘     └─
st   ────────────────────────────────────────────────────────────
467      (veq : (v1 = [] ∧ ¬ contains_aux a bkt) ∨ ∃b'', v1 = [⟨a, b''⟩]),
id                         └──────────┘   └─┘                    
src  ──────────┘      └──────────┘    └┘└─┘     └┘    
typ  ──────────┘      └──────────┘ └─┘└┘└─┘     └┘    
doc  ──────────┘        └──────────┘    └┘  └─┘       └┘     
txt  ──────────┘                        └┘  └─┘       └┘     
par  ──────────┘                        └┘  └─┘       └┘     
pid  ──────────┘                        └┘  └─┘       └┘     
st   ──────────────────────────────────────────────────────────────────────
468      sigma.mk a' b' ∈ bkts'.as_list ↔
id                            └──────┘
src  ───┘                 └──────┘ 
typ  ───┘                 └──────┘ 
doc  ───┘                  └──────┘ 
txt  ───┘                           
par  ───┘                           
pid  ───┘                           
st   ─────────────────────────────────────
469      if a = a' then b == b' else sigma.mk a' b' ∈ bkts.as_list,
id                       └┘         └──────┘ └┘ └┘   └──────────┘
src  ───┘  └─┘   └────┘ └┘  └────┘└──────┘     └──────────┘
typ  ───┘  └─┘   └────┘└┘  └────┘└──────┘└┘└┘ └──────────┘
doc  ───┘  └─┘   └────┘     └────┘             └──────────┘
txt  ───┘  └─┘   └────┘     └────┘             
par  ───┘  └─┘   └────┘     └────┘             
pid  ───┘  └─┘   └────┘     └────┘             
st   ────────────────────────────────────────────────────────────┘└─
470    { intros bkts' v1 u w hl hfl veq,
src      └────────────────────────────┘
typ      └────────────────────────────┘
doc      └────────────────────────────┘
txt      └────────────────────────────┘
par      └────────────────────────────┘
pid            └──────────────────────┘
st   ───┘└────────────────────────────┘└─
471      rw [hl, hfl],
id           └┘  └─┘
src      └──┘  └┘   
typ      └──┘└┘└┘└─┘
doc      └──┘  └┘   
txt      └──┘  └┘   
par      └──┘  └┘   
pid        └┘  └┘   
st   ─────────┘└───┘└──
472      by_cases h : a = a',
id                       └┘
src      └───────┘ └─┘  
typ      └───────┘ └─┘ └┘
doc      └───────┘ └─┘  
txt      └───────┘ └─┘  
par      └───────┘ └─┘  
pid               └─┘  
st   ──────────────────────┘└─
473      { subst a',
id               └┘
src        └────┘
typ        └────┘└┘
doc        └────┘
txt        └────┘
par        └────┘
pid             
st   ─────┘└──────┘└─
474        suffices : b = b' ∨ sigma.mk a b' ∈ u ∨ sigma.mk a b' ∈ w ↔ b = b',
id                                                └──────┘             └┘
src        └─────────┘                   └──────┘        
typ        └─────────┘                  └──────┘     └┘
doc        └─────────┘                                   
txt        └─────────┘                                   
par        └─────────┘                                   
pid        └───────┘└┘                                   
st   ───────────────────────────────────────────────────────────────────────┘└─
475        { simpa [eq_comm, or.left_comm] },
id                  └─────┘  └──────────┘
src          └─────┘└─────┘└┘└──────────┘└┘
typ          └─────┘└─────┘└┘└──────────┘└┘
doc          └─────┘       └┘            └┘
txt          └─────┘       └┘            └┘
par          └─────┘       └┘            └┘
pid                      └┘            
st   ───────┘└────────────────────────────┘└┘
476        refine or_iff_left_of_imp (not.elim $ not_or_distrib.2 _),
id                └────────────────┘  └──────┘   └────────────┘
src        └─────┘└────────────────┘ └──────┘ └────────────┘└───┘
typ        └─────┘└────────────────┘ └──────┘ └────────────┘└───┘
doc        └─────┘                                          └───┘
txt        └─────┘                                          └───┘
par        └─────┘                                          └───┘
pid                                                        └───┘
st   ──────────────────────────────────────────────────────────────┘└─
477        rcases veq with ⟨rfl, Hnc⟩ | ⟨b'', rfl⟩,
id                └─┘
src        └─────┘   └───────────────────────────┘
typ        └─────┘└─┘└───────────────────────────┘
doc        └─────┘   └───────────────────────────┘
txt        └─────┘   └───────────────────────────┘
par        └─────┘   └───────────────────────────┘
pid                 └───────────────────────────┘
st   ────────────────────────────────────────────┘└─
478        { have na := (not_iff_not_of_iff $ v.contains_aux_iff _ _).1 Hnc,
id                       └────────────────┘   └────────────────┘        └─┘
src          └─────────┘ └────────────────┘ └────────────────┘└──────┘
typ          └─────────┘ └────────────────┘ └────────────────┘└──────┘└─┘
doc          └─────────┘                                      └──────┘
txt          └─────────┘                                      └──────┘
par          └─────────┘                                      └──────┘
pid          └─────┘└─┘                                      └──────┘
st   ───────┘└────────────────────────────────────────────────────────────┘└─
479          simp [hl, not_or_distrib] at na, simp [na] },
id                 └┘  └────────────┘               └┘
src          └────┘  └┘└────────────┘└─────┘  └────┘  └┘
typ          └────┘└┘└┘└────────────┘└─────┘  └────┘└┘└┘
doc          └────┘  └┘              └─────┘  └────┘  └┘
txt          └────┘  └┘              └─────┘  └────┘  └┘
par          └────┘  └┘              └─────┘  └────┘  └┘
pid                └┘              └───┘        
st   ──────────────────────────────────────┘└──────────┘└┘
480        { have nd' := v.as_list_nodup _,
id                       └─────────────┘
src          └──────────┘└─────────────┘└┘
typ          └──────────┘└─────────────┘└┘
doc          └──────────┘               └┘
txt          └──────────┘               └┘
par          └──────────┘               └┘
pid          └──────┘└─┘               └┘
st   ────────────────────────────────────┘└─
481          simp [hl, list.nodup_append] at nd', simp [nd'] } },
id                 └┘  └───────────────┘                └─┘
src          └────┘  └┘└───────────────┘└──────┘  └────┘   └┘
typ          └────┘└┘└┘└───────────────┘└──────┘  └────┘└─┘└┘
doc          └────┘  └┘                 └──────┘  └────┘   └┘
txt          └────┘  └┘                 └──────┘  └────┘   └┘
par          └────┘  └┘                 └──────┘  └────┘   └┘
pid                └┘                 └────┘         
st   ──────────────────────────────────────────┘└───────────┘└──┘
482      { suffices : sigma.mk a' b' ∉ v1, {simp [h, ne.symm h, this]},
id                    └──────┘ └┘ └┘   └┘           └─────┘   └──┘
src        └─────────┘└──────┘          └────┘ └┘└─────┘ └┘    
typ        └─────────┘└──────┘└┘└┘ └┘   └────┘└┘└─────┘└┘└──┘
doc        └─────────┘                  └────┘ └┘        └┘    
txt        └─────────┘                  └────┘ └┘        └┘    
par        └─────────┘                  └────┘ └┘        └┘    
pid        └───────┘└┘                       └┘        └┘    
st   ───────────────────────────────────┘└──────────────────────────┘└┘
483        rcases veq with ⟨rfl, Hnc⟩ | ⟨b'', rfl⟩; simp [ne.symm h] } },
id                └─┘                                     └─────┘ 
src        └─────┘   └───────────────────────────┘  └────┘└─────┘ └┘
typ        └─────┘└─┘└───────────────────────────┘  └────┘└─────┘└┘
doc        └─────┘   └───────────────────────────┘  └────┘        └┘
txt        └─────┘   └───────────────────────────┘  └────┘        └┘
par        └─────┘   └───────────────────────────┘  └────┘        └┘
pid                 └───────────────────────────┘              
st   ───────────────────────────────────────────────────────────────┘└──┘
484    by_cases Hc : (contains_aux a bkt : Prop),
id                    └──────────┘  └─┘
src    └───────┘  └─┘ └──────────┘    └─┘    
typ    └───────┘  └─┘ └──────────┘└─┘└─┘    
doc    └───────┘  └─┘ └──────────┘    └─┘    
txt    └───────┘  └─┘                 └─┘    
par    └───────┘  └─┘                 └─┘    
pid              └─┘                 └─┘    
st   ──────────────────────────────────────────┘└─
485    { rcases hash_map.valid.replace_aux a b (array.read bkts (mk_idx n (hash_fn a)))
id              └────────────────────────┘     └────────┘ └──┘  └────┘   └─────┘ 
src      └─────┘└────────────────────────┘   └────────┘     └────┘          └───
typ      └─────┘└────────────────────────┘  └────────┘└──┘ └────┘ └─────┘└───
doc      └─────┘                                            └────┘          └───
txt      └─────┘                                                            └───
par      └─────┘                                                            └───
pid                                                                        └───
st   ───┘└──────────────────────────────────────────────────────────────────────────────
486        ((contains_aux_iff nd).1 Hc) with ⟨u', w', b'', hl', hfl'⟩,
id           └──────────────┘ └┘    └┘
src  ─────┘  └──────────────┘  └──┘  └─────────────────────────────┘
typ  ─────┘  └──────────────┘└┘└──┘└┘└─────────────────────────────┘
doc  ─────┘                    └──┘  └─────────────────────────────┘
txt  ─────┘                    └──┘  └─────────────────────────────┘
par  ─────┘                    └──┘  └─────────────────────────────┘
pid  ─────┘                    └──┘  └─────────────────────────────┘
st   ───────────────────────────────────────────────────────────────┘└─
487      rcases (append_of_modify u' [⟨a, b''⟩] [⟨a, b⟩] w' hl' hfl') with ⟨u, w, hl, hfl⟩,
id               └──────────────┘ └┘      └─┘        └┘ └─┘ └──┘
src      └─────┘ └──────────────┘     └┘      └┘          └────────────────────┘
typ      └─────┘ └──────────────┘└┘   └┘└─┘  └┘└┘└─┘└──┘└────────────────────┘
doc      └─────┘                      └┘       └┘           └────────────────────┘
txt      └─────┘                      └┘       └┘           └────────────────────┘
par      └─────┘                      └┘       └┘           └────────────────────┘
pid                                  └┘       └┘           └────────────────────┘
st   ────────────────────────────────────────────────────────────────────────────────────┘└─
488      simpa [insert, @dif_pos (contains_aux a bkt) _ Hc]
id              └────┘   └─────┘  └──────────┘  └─┘    └┘
src      └─────┘└────┘└┘ └─────┘ └──────────┘    └──┘  └─
typ      └─────┘└────┘└┘ └─────┘ └──────────┘└─┘└──┘└┘└─
doc      └─────┘└────┘└┘         └──────────┘    └──┘  └─
txt      └─────┘      └┘                         └──┘  └─
par      └─────┘      └┘                         └──┘  └─
pid                 └┘                         └──┘  
st   ───────────────────────────────────────────────────────
489        using lem _ _ u w hl hfl (or.inr ⟨b'', rfl⟩) },
id               └─┘       └┘ └─┘  └────┘  └─┘  └─┘
src  ───────────┘   └───┘        └────┘    └┘└─┘└─┘
typ  ───────────┘└─┘└───┘└┘└─┘ └────┘ └─┘└┘└─┘└─┘
doc  ───────────┘   └───┘                  └┘   └─┘
txt  ───────────┘   └───┘                  └┘   └─┘
par  ───────────┘   └───┘                  └┘   └─┘
pid  ─────┘└────┘   └───┘                  └┘   └┘
st   ──────────────────────────────────────────────────┘└┘
490    { let size' := size + 1,
id                    └──┘ 
src      └───────────┘    └┘
typ      └───────────┘└──┘└┘
doc      └───────────┘     └┘
txt      └───────────┘     └┘
par      └───────────┘     └┘
pid      └───────┘└─┘     
st   ────────────────────────┘└─
491      let bkts' := bkts.modify hash_fn a (λl, ⟨a, b⟩::l),
id                    └─────────┘ └─────┘           
src      └───────────┘└─────────┘          └─┘  └┘    
typ      └───────────┘└─────────┘└─────┘   └─┘ └┘   
doc      └───────────┘└─────────┘          └─┘  └┘    
txt      └───────────┘                     └─┘  └┘    
par      └───────────┘                     └─┘  └┘    
pid      └───────┘└─┘                     └─┘  └┘    
st   ─────────────────────────────────────────────────────┘└─
492      have mi : sigma.mk a' b' ∈ bkts'.as_list ↔
id                                  └───────────┘
src      └────────┘             └───────────┘ 
typ      └────────┘             └───────────┘ 
doc      └────────┘             └───────────┘ 
txt      └────────┘                           
par      └────────┘                           
pid      └─────┘└─┘                           
st   ───────────────────────────────────────────────
493          if a = a' then b == b' else sigma.mk a' b' ∈ bkts.as_list :=
id                                      └──────┘ └┘ └┘   └──────────┘
src  ───────┘  └─┘   └────┘     └────┘└──────┘     └──────────┘└───
typ  ───────┘  └─┘   └────┘    └────┘└──────┘└┘└┘ └──────────┘└───
doc  ───────┘  └─┘   └────┘     └────┘             └──────────┘└───
txt  ───────┘  └─┘   └────┘     └────┘                         └───
par  ───────┘  └─┘   └────┘     └────┘                         └───
pid  ───────┘  └─┘   └────┘     └────┘                         └───
st   ─────────────────────────────────────────────────────────────────────
494        let ⟨u, w, hl, hfl⟩ := append_of_modify [] [] [⟨a, b⟩] _ rfl rfl in
id                  └┘  └─┘     └──────────────┘                    └─┘
src  ─────┘     └┘ └┘  └┘   └───┘└──────────────┘       └┘  └─┘   └─┘└───
typ  ─────┘    └┘└┘└┘└┘└─┘└───┘└──────────────┘      └┘ └─┘   └─┘└───
doc  ─────┘     └┘ └┘  └┘   └───┘                       └┘  └─┘      └───
txt  ─────┘     └┘ └┘  └┘   └───┘                       └┘  └─┘      └───
par  ─────┘     └┘ └┘  └┘   └───┘                       └┘  └─┘      └───
pid  ─────┘     └┘ └┘  └┘   └───┘                       └┘  └─┘      └───
st   ──────────────────────────────────────────────────────────────────────────
495        lem bkts' _ u w hl hfl $ or.inl ⟨rfl, Hc⟩,
id         └─┘ └───┘                └────┘       └┘
src  ─────┘        └─┘        └────┘    └┘  
typ  ─────┘└─┘└───┘└─┘        └────┘    └┘└┘
doc  ─────┘        └─┘                  └┘  
txt  ─────┘        └─┘                  └┘  
par  ─────┘        └─┘                  └┘  
pid  ─────┘        └─┘                  └┘  
st   ──────────────────────────────────────────────┘└─
496      simp [insert, @dif_neg (contains_aux a bkt) _ Hc],
id             └────┘   └─────┘  └──────────┘  └─┘    └┘
src      └────┘└────┘└┘ └─────┘ └──────────┘    └──┘  
typ      └────┘└────┘└┘ └─────┘ └──────────┘└─┘└──┘└┘
doc      └────┘└────┘└┘         └──────────┘    └──┘  
txt      └────┘      └┘                         └──┘  
par      └────┘      └┘                         └──┘  
pid                └┘                         └──┘  
st   ────────────────────────────────────────────────────┘└─
497      by_cases h : size' ≤ n.1,
id                    └───┘  
src      └───────┘ └─┘      └┘
typ      └───────┘ └─┘└───┘└┘
doc      └───────┘ └─┘       └┘
txt      └───────┘ └─┘       └┘
par      └───────┘ └─┘       └┘
pid               └─┘       └┘
st   ───────────────────────────┘└─
498      -- TODO(Mario): Why does the by_cases assumption look different than the stated one?
st   ─────────────────────────────────────────────────────────────────────────────────────────
499      { simpa [show size' ≤ n.1, from h] using mi },
id                     └───┘                    └┘
src        └─────┘           └───────┘ └──────┘  
typ        └─────┘    └───┘ └───────┘└──────┘└┘
doc        └─────┘           └───────┘ └──────┘  
txt        └─────┘           └───────┘ └──────┘  
par        └─────┘           └───────┘ └──────┘  
pid                        └───────┘ └────┘  
st   ─────┘└────────────────────────────────────────┘└┘
500      { let n' : ℕ+ := ⟨n.1 * 2, mul_pos n.2 dec_trivial⟩,
id                  └┘             └─────┘    └─────────┘
src        └───────┘└┘└──┘  └─┘└──┘└─────┘ └─┘└─────────┘
typ        └───────┘└┘└──┘  └─┘└──┘└─────┘└─┘└─────────┘
doc        └───────┘└┘└──┘  └─┘ └──┘        └─┘└─────────┘
txt        └───────┘  └──┘  └─┘ └──┘        └─┘           
par        └───────┘  └──┘  └─┘ └──┘        └─┘           
pid        └────┘└─┘  └──┘  └─┘ └──┘        └─┘           
st   ──────────────────────────────────────────────────────┘└─
501        let bkts'' : bucket_array α β n' := bkts'.foldl (mk_array _ []) (reinsert_aux hash_fn),
id                      └──────────┘   └┘    └─────────┘  └──────┘        └──────────┘ └─────┘
src        └───────────┘└──────────┘    └──┘└─────────┘ └──────┘└─┘  └┘ └──────────┘       
typ        └───────────┘└──────────┘└┘└──┘└─────────┘ └──────┘└─┘  └┘ └──────────┘└─────┘
doc        └───────────┘└──────────┘    └──┘└─────────┘         └─┘  └┘ └──────────┘       
txt        └───────────┘                └──┘                    └─┘  └┘                    
par        └───────────┘                └──┘                    └─┘  └┘                    
pid        └────────┘└─┘                └──┘                    └─┘  └┘                    
st   ───────────────────────────────────────────────────────────────────────────────────────────┘└─
502        suffices : sigma.mk a' b' ∈ bkts''.as_list ↔ sigma.mk a' b' ∈ bkts'.as_list.reverse,
id                                     └────────────┘   └──────┘ └┘ └┘   └───────────────────┘
src        └─────────┘             └────────────┘ └──────┘     └───────────────────┘
typ        └─────────┘             └────────────┘ └──────┘└┘└┘ └───────────────────┘
doc        └─────────┘             └────────────┘              └───────────────────┘
txt        └─────────┘                                         
par        └─────────┘                                         
pid        └───────┘└┘                                         
st   ────────────────────────────────────────────────────────────────────────────────────────┘└─
503        { simpa [show ¬ size' ≤ n.1, from h, mi] },
id                        └───┘              └┘
src          └─────┘            └───────┘ └┘  └┘
typ          └─────┘    └───┘ └───────┘└┘└┘└┘
doc          └─────┘            └───────┘ └┘  └┘
txt          └─────┘            └───────┘ └┘  └┘
par          └─────┘            └───────┘ └┘  └┘
pid                           └───────┘ └┘  
st   ───────┘└─────────────────────────────────────┘└┘
504        rw [show bkts'' = bkts'.as_list.foldl _ _, from bkts'.foldl_eq _ _,
id                  └────┘  └─────────────────┘           └────────────┘
src        └──┘           └─────────────────┘└─────────┘└────────────┘└─────
typ        └──┘    └────┘└─────────────────┘└─────────┘└────────────┘└─────
doc        └──┘           └─────────────────┘└─────────┘              └─────
txt        └──┘                              └─────────┘              └─────
par        └──┘                              └─────────┘              └─────
pid          └┘                              └─────────┘              └─────
st   ───────────────────────────────────────────────────────────────────────┘└─
505            ← list.foldr_reverse],
id               └────────────────┘
src  ───────────┘└────────────────┘
typ  ───────────┘└────────────────┘
doc  ───────────┘                  
txt  ───────────┘                  
par  ───────────┘                  
pid  ───────────┘                  
st   ─────────────────────────────┘└──
506        induction bkts'.as_list.reverse with a l IH,
id                   └───────────────────┘
src        └────────┘└───────────────────┘└──────────┘
typ        └────────┘└───────────────────┘└──────────┘
doc        └────────┘└───────────────────┘└──────────┘
txt        └────────┘                     └──────────┘
par        └────────┘                     └──────────┘
pid                                      └─────────┘
st   ────────────────────────────────────────────────┘└─
507        { simp [mk_as_list] },
id                 └────────┘
src          └────┘└────────┘└┘
typ          └────┘└────────┘└┘
doc          └────┘          └┘
txt          └────┘          └┘
par          └────┘          └┘
pid                        
st   ───────┘└────────────────┘└┘
508        { cases a with a'' b'',
id                 
src          └────┘ └───────────┘
typ          └────┘└───────────┘
doc          └────┘ └───────────┘
txt          └────┘ └───────────┘
par          └────┘ └───────────┘
pid                └───────────┘
st   ───────────────────────────┘└─
509          let B := l.foldr (λ (y : sigma β) (x : bucket_array α β n'),
id                    └─────┘         └───┘         └──────────┘  
src          └───────┘└─────┘  └────┘└───┘ └─────┘└──────────┘    └──
typ          └───────┘└─────┘  └────┘└───┘ └─────┘└──────────┘  └──
doc          └───────┘         └────┘      └─────┘└──────────┘    └──
txt          └───────┘         └────┘      └─────┘                └──
par          └───────┘         └────┘      └─────┘                └──
pid          └───┘└─┘         └────┘      └─────┘                └──
st   ─────────────────────────────────────────────────────────────────────
510            reinsert_aux hash_fn x y.1 y.2) (mk_array n'.1 []),
id             └──────────┘ └─────┘             └──────┘ └┘   └┘
src  ─────────┘└──────────┘         └─┘ └──┘ └──────┘  └─┘└┘
typ  ─────────┘└──────────┘└─────┘  └─┘ └──┘ └──────┘└┘└─┘└┘
doc  ─────────┘└──────────┘         └─┘ └──┘           └─┘  
txt  ─────────┘                     └─┘ └──┘           └─┘  
par  ─────────┘                     └─┘ └──┘           └─┘  
pid  ─────────┘                     └─┘ └──┘           └─┘  
st   ───────────────────────────────────────────────────────────┘└─
511          rcases append_of_modify [] [] [⟨a'', b''⟩] _ rfl rfl with ⟨u, w, hl, hfl⟩,
id                  └──────────────┘        └─┘  └─┘        └─┘
src          └─────┘└──────────────┘        └┘   └─┘   └─┘└───────────────────┘
typ          └─────┘└──────────────┘     └─┘└┘└─┘└─┘   └─┘└───────────────────┘
doc          └─────┘                         └┘    └─┘      └───────────────────┘
txt          └─────┘                         └┘    └─┘      └───────────────────┘
par          └─────┘                         └┘    └─┘      └───────────────────┘
pid                                         └┘    └─┘      └───────────────────┘
st   ────────────────────────────────────────────────────────────────────────────────┘└─
512          simp [IH.symm, or.left_comm, show B.as_list = _, from hl,
id                          └──────────┘       └───────┘          └┘
src          └────┘       └┘└──────────┘└┘    └───────┘ └───────┘  └─
typ          └────┘└─────┘└┘└──────────┘└┘    └───────┘└───────┘└┘└─
doc          └────┘       └┘            └┘    └───────┘ └───────┘  └─
txt          └────┘       └┘            └┘              └───────┘  └─
par          └────┘       └┘            └┘              └───────┘  └─
pid                     └┘            └┘              └───────┘  └─
st   ──────────────────────────────────────────────────────────────────
513                show (reinsert_aux hash_fn B a'' b'').as_list = _, from hfl] } } }
id                       └──────────┘ └─────┘  └─┘ └─┘                   └─┘
src  ─────────────┘     └──────────┘              └────────┘ └───────┘   └┘
typ  ─────────────┘     └──────────┘└─────┘└─┘└─┘└────────┘└───────┘└─┘└┘
doc  ─────────────┘     └──────────┘              └────────┘ └───────┘   └┘
txt  ─────────────┘                               └────────┘ └───────┘   └┘
par  ─────────────┘                               └────────┘ └───────┘   └┘
pid  ─────────────┘                               └────────┘ └───────┘   
st   ──────────────────────────────────────────────────────────────────────────┘└─────
514  end
st   ──┘
515  
516  theorem find_insert_eq (m : hash_map α β) (a : α) (b : β a) : (m.insert a b).find a = some b :=
id                               └──────┘                      └─────┘   └──┘    └──┘ 
src                              └──────┘                            └─────┘     └──┘     └──┘
typ                              └──────┘                      └─────┘   └──┘    └──┘ 
doc                              └──────┘                            └─────┘     └──┘
517  (find_iff (m.insert a b) a b).2 $ (mem_insert m a b a b).2 $ by rw if_pos rfl
id    └──────┘  └─────┘           └────────┘                └────┘ └─┘
src   └──────┘   └─────┘               └────────┘                  └─┘└────┘└─┘
typ   └──────┘  └─────┘           └────────┘             └─┘└────┘└─┘
doc              └─────┘                                             └─┘         
txt                                                                  └─┘         
par                                                                  └─┘         
pid                                                                             
st                                                                  └──────────────
518  
src  
typ  
doc  
txt  
par  
pid  
st   
519  theorem find_insert_ne (m : hash_map α β) (a a' : α) (b : β a) (h : a ≠ a') :
id                               └──────┘                             └┘
src                              └──────┘                                  
typ                              └──────┘                             └┘
doc                              └──────┘
520    (m.insert a b).find a' = m.find a' :=
id      └─────┘   └──┘  └┘  └───┘ └┘
src      └─────┘     └──┘       └───┘
typ     └─────┘   └──┘  └┘  └───┘ └┘
doc      └─────┘     └──┘        └───┘
521  option.eq_of_eq_some $ λb',
id   └──────────────────┘    └┘
src  └──────────────────┘
typ  └──────────────────┘    └┘
522  let t := mem_insert m a b a' b' in
id           └────────┘    └┘ └┘
src           └────────┘
typ          └────────┘    └┘ └┘
523  (find_iff _ _ _).trans $ iff.trans (by rwa if_neg h at t) (find_iff _ _ _).symm
id    └──────┘       └───┘    └───────┘         └────┘         └──────┘       └──┘
src   └──────┘       └───┘    └───────┘     └──┘└────┘ └───┘   └──────┘       └──┘
typ   └──────┘       └───┘    └───────┘     └──┘└────┘└───┘   └──────┘       └──┘
doc                                         └──┘       └───┘
txt                                         └──┘       └───┘
par                                         └──┘       └───┘
pid                                                   └───┘
st                                         └────────────────┘
524  
525  theorem find_insert (m : hash_map α β) (a' a : α) (b : β a) :
id                            └──────┘                    
src                           └──────┘
typ                           └──────┘                    
doc                           └──────┘
526    (m.insert a b).find a' = if h : a = a' then some (eq.rec_on h b) else m.find a' :=
id      └─────┘   └──┘  └┘  └┘       └┘      └──┘  └───────┘         └───┘ └┘
src      └─────┘     └──┘      └┘                └──┘  └───────┘            └───┘
typ     └─────┘   └──┘  └┘  └┘       └┘      └──┘  └───────┘         └───┘ └┘
doc      └─────┘     └──┘                                                     └───┘
527  if h : a = a' then by rw dif_pos h; exact
id   └┘       └┘            └─────┘ 
src  └┘                   └─┘└─────┘   └─────
typ  └┘       └┘         └─┘└─────┘  └─────
doc                        └─┘          └─────
txt                        └─┘          └─────
par                        └─┘          └─────
pid                                         
st                        └────────────────────
528    match a', h with ._, rfl := find_insert_eq m a b end
id           └┘            └─┘    └────────────┘   
src  ─┘       └┘ └────┘  └┘└─┘└──┘└────────────┘   └───┘
typ  ─┘     └┘└┘└────┘  └┘└─┘└──┘└────────────┘└───┘
doc  ─┘       └┘ └────┘  └┘   └──┘                 └───┘
txt  ─┘       └┘ └────┘  └┘   └──┘                 └───┘
par  ─┘       └┘ └────┘  └┘   └──┘                 └───┘
pid  ─┘       └┘ └────┘  └┘   └──┘                 └──┘
st   ──────────────────────────────────────────────────────┘
529  else by rw dif_neg h; exact find_insert_ne m a a' b h
id              └─────┘         └────────────┘   └┘  
src          └─┘└─────┘   └────┘└────────────┘      
typ          └─┘└─────┘  └────┘└────────────┘└┘
doc          └─┘          └────┘                    
txt          └─┘          └────┘                    
par          └─┘          └────┘                    
pid                                               
st          └──────────────────────────────────────────────
530  
src  
typ  
doc  
txt  
par  
pid  
st   
531  /-- Insert a list of key-value pairs into the map. (Modifies `m` in-place when applicable) -/
532  def insert_all (l : list (Σ a, β a)) (m : hash_map α β) : hash_map α β :=
id                       └──┘             └──────┘      └──────┘  
src                      └──┘                └──────┘        └──────┘
typ                      └──┘             └──────┘      └──────┘  
doc                                            └──────┘        └──────┘
533  l.foldl (λ m ⟨a, b⟩, insert m a b) m
id   └────┘          └────┘       
src   └────┘              └────┘
typ  └────┘          └────┘       
doc                       └────┘
534  
535  /-- Construct a hash map from a list of key-value pairs. -/
536  def of_list (l : list (Σ a, β a)) (hash_fn) : hash_map α β :=
id                    └──┘                    └──────┘  
src                   └──┘                       └──────┘
typ                   └──┘                    └──────┘  
doc                                                └──────┘
537  insert_all l (mk_hash_map hash_fn (2 * l.length))
id   └────────┘   └─────────┘ └─────┘     └─────┘
src  └────────┘    └─────────┘              └─────┘
typ  └────────┘   └─────────┘ └─────┘     └─────┘
doc  └────────┘    └─────────┘
538  
539  /-- Remove a key from the map. (Modifies `m` in-place when applicable) -/
540  def erase (m : hash_map α β) (a : α) : hash_map α β :=
id                  └──────┘             └──────┘  
src                 └──────┘                └──────┘
typ                 └──────┘             └──────┘  
doc                 └──────┘                └──────┘
541  match m with ⟨hash_fn, size, n, buckets, v⟩ :=
id                └─────┘  └──┘    └─────┘  
typ               └─────┘  └──┘    └─────┘  
542    if hc : contains_aux a (buckets.read hash_fn a) then
id     └┘      └──────────┘          └───┘         
src    └┘      └──────────┘           └───┘
typ    └┘      └──────────┘          └───┘         
doc            └──────────┘           └───┘
543    { hash_fn  := hash_fn,
544      size     := size - 1,
id                        
src                       
typ                       
545      nbuckets := n,
546      buckets  := buckets.modify hash_fn a (erase_aux a),
id                          └─────┘           └───────┘ 
src                         └─────┘            └───────┘
typ                         └─────┘           └───────┘ 
doc                         └─────┘            └───────┘
547      is_valid := v.erase _ a hc }
id                    └────┘    └┘
src                   └────┘
typ                   └────┘    └┘
548    else m
id          
typ         
549  end
550  
551  theorem mem_erase : Π (m : hash_map α β) (a a' b'),
id                             └──────┘      └┘ └┘
src                             └──────┘
typ                            └──────┘      └┘ └┘
doc                             └──────┘
552    (sigma.mk a' b' : sigma β) ∈ (m.erase a).entries ↔
id      └──────┘ └┘ └┘   └───┘     └────┘  └─────┘  
src     └──────┘         └───┘       └────┘   └─────┘  
typ     └──────┘ └┘ └┘   └───┘     └────┘  └─────┘  
doc                                   └────┘   └─────┘
553    a ≠ a' ∧ sigma.mk a' b' ∈ m.entries
id       └┘  └──────┘ └┘ └┘  └──────┘
src           └──────┘         └──────┘
typ      └┘  └──────┘ └┘ └┘  └──────┘
doc                               └──────┘
554  | ⟨hash_fn, size, n, bkts, v⟩ a a' b' := begin
st                                            └─────
555    let bkt := bkts.read hash_fn a,
id                └───────┘ └─────┘ 
src    └─────────┘└───────┘       
typ    └─────────┘└───────┘└─────┘
doc    └─────────┘└───────┘       
txt    └─────────┘                
par    └─────────┘                
pid    └─────┘└─┘                
st   ───────────────────────────────┘└─
556    by_cases Hc : (contains_aux a bkt : Prop),
id                    └──────────┘  └─┘
src    └───────┘  └─┘ └──────────┘    └─┘    
typ    └───────┘  └─┘ └──────────┘└─┘└─┘    
doc    └───────┘  └─┘ └──────────┘    └─┘    
txt    └───────┘  └─┘                 └─┘    
par    └───────┘  └─┘                 └─┘    
pid              └─┘                 └─┘    
st   ──────────────────────────────────────────┘└─
557    { let bkts' := bkts.modify hash_fn a (erase_aux a),
id                    └─────────┘ └─────┘    └───────┘ 
src      └───────────┘└─────────┘         └───────┘ 
typ      └───────────┘└─────────┘└─────┘  └───────┘
doc      └───────────┘└─────────┘         └───────┘ 
txt      └───────────┘                              
par      └───────────┘                              
pid      └───────┘└─┘                              
st   ───┘└──────────────────────────────────────────────┘└─
558      suffices : sigma.mk a' b' ∈ bkts'.as_list ↔ a ≠ a' ∧ sigma.mk a' b' ∈ bkts.as_list,
id                                  └───────────┘          └──────┘ └┘ └┘   └──────────┘
src      └─────────┘            └───────────┘     └──────┘     └──────────┘
typ      └─────────┘            └───────────┘    └──────┘└┘└┘ └──────────┘
doc      └─────────┘             └───────────┘                   └──────────┘
txt      └─────────┘                                             
par      └─────────┘                                             
pid      └───────┘└┘                                             
st   ─────────────────────────────────────────────────────────────────────────────────────┘└─
559      { simpa [erase, @dif_pos (contains_aux a bkt) _ Hc] },
id                └───┘   └─────┘  └──────────┘  └─┘    └┘
src        └─────┘└───┘└┘ └─────┘ └──────────┘    └──┘  └┘
typ        └─────┘└───┘└┘ └─────┘ └──────────┘└─┘└──┘└┘└┘
doc        └─────┘└───┘└┘         └──────────┘    └──┘  └┘
txt        └─────┘     └┘                         └──┘  └┘
par        └─────┘     └┘                         └──┘  └┘
pid                  └┘                         └──┘  
st   ─────┘└────────────────────────────────────────────────┘└┘
560      have nd := v.nodup (mk_idx n (hash_fn a)),
id                  └─────┘  └────┘   └─────┘ 
src      └─────────┘└─────┘ └────┘          └┘
typ      └─────────┘└─────┘ └────┘ └─────┘└┘
doc      └─────────┘        └────┘          └┘
txt      └─────────┘                        └┘
par      └─────────┘                        └┘
pid      └─────┘└─┘                        └┘
st   ────────────────────────────────────────────┘└─
561      rcases valid.erase_aux a bkt ((contains_aux_iff nd).1 Hc) with ⟨u', w', b, hl', hfl'⟩,
id              └─────────────┘  └─┘   └──────────────┘ └┘    └┘
src      └─────┘└─────────────┘      └──────────────┘  └──┘  └───────────────────────────┘
typ      └─────┘└─────────────┘└─┘  └──────────────┘└┘└──┘└┘└───────────────────────────┘
doc      └─────┘                                       └──┘  └───────────────────────────┘
txt      └─────┘                                       └──┘  └───────────────────────────┘
par      └─────┘                                       └──┘  └───────────────────────────┘
pid                                                   └──┘  └───────────────────────────┘
st   ────────────────────────────────────────────────────────────────────────────────────────┘└─
562      rcases append_of_modify u' [⟨a, b⟩] [] _ hl' hfl' with ⟨u, w, hl, hfl⟩,
id              └──────────────┘ └┘      └┘   └─┘ └──┘
src      └─────┘└──────────────┘    └┘ └┘└─┘       └───────────────────┘
typ      └─────┘└──────────────┘└┘ └┘└┘└─┘└─┘└──┘└───────────────────┘
doc      └─────┘                     └┘    └─┘       └───────────────────┘
txt      └─────┘                     └┘    └─┘       └───────────────────┘
par      └─────┘                     └┘    └─┘       └───────────────────┘
pid                                 └┘    └─┘       └───────────────────┘
st   ─────────────────────────────────────────────────────────────────────────┘└─
563      suffices : ∀_:sigma.mk a' b' ∈ u ∨ sigma.mk a' b' ∈ w, a ≠ a',
id                                        └──────┘    └┘        └┘
src      └─────────┘ └┘               └──────┘         
typ      └─────────┘ └┘             └──────┘  └┘   └┘
doc      └─────────┘ └┘                                
txt      └─────────┘ └┘                                
par      └─────────┘ └┘                                
pid      └───────┘└┘ └┘                                
st   ────────────────────────────────────────────────────────────────┘└─
564      { have : sigma.mk a' b' ∈ u ∨ sigma.mk a' b' ∈ w ↔ (¬a = a' ∧ a' = a) ∧ b' == b ∨
id                                                                                 └┘ 
src        └─────┘                                        └┘   └┘  
typ        └─────┘                                        └┘   └┘ 
doc        └─────┘                                         └┘       
txt        └─────┘                                         └┘       
par        └─────┘                                         └┘       
pid        └───┘└┘                                         └┘       
st   ─────┘└───────────────────────────────────────────────────────────────────────────────
565          ¬a = a' ∧ (sigma.mk a' b' ∈ u ∨ sigma.mk a' b' ∈ w),
id                                         └──────┘ └┘ └┘   
src  ───────┘                      └──────┘      
typ  ───────┘                    └──────┘└┘└┘ 
doc  ───────┘                                    
txt  ───────┘                                    
par  ───────┘                                    
pid  ───────┘                                    
st   ──────────────────────────────────────────────────────────┘└─
566        { simp [eq_comm, not_and_self_iff, and_iff_right_of_imp this] },
id                 └─────┘  └──────────────┘  └──────────────────┘ └──┘
src          └────┘└─────┘└┘└──────────────┘└┘└──────────────────┘    └┘
typ          └────┘└─────┘└┘└──────────────┘└┘└──────────────────┘└──┘└┘
doc          └────┘       └┘                └┘                        └┘
txt          └────┘       └┘                └┘                        └┘
par          └────┘       └┘                └┘                        └┘
pid                     └┘                └┘                        
st   ───────┘└──────────────────────────────────────────────────────────┘└┘
567        simpa [hl, show bkts'.as_list = _, from hfl, and_or_distrib_left,
id                └┘       └───────────┘          └─┘  └─────────────────┘
src        └─────┘  └┘    └───────────┘ └───────┘   └┘└─────────────────┘└─
typ        └─────┘└┘└┘    └───────────┘└───────┘└─┘└┘└─────────────────┘└─
doc        └─────┘  └┘    └───────────┘ └───────┘   └┘                   └─
txt        └─────┘  └┘                  └───────┘   └┘                   └─
par        └─────┘  └┘                  └───────┘   └┘                   └─
pid               └┘                  └───────┘   └┘                   └─
st   ────────────────────────────────────────────────────────────────────────
568               and_comm, and.left_comm, or.left_comm] },
id                └──────┘  └───────────┘  └──────────┘
src  ────────────┘└──────┘└┘└───────────┘└┘└──────────┘└┘
typ  ────────────┘└──────┘└┘└───────────┘└┘└──────────┘└┘
doc  ────────────┘        └┘             └┘            └┘
txt  ────────────┘        └┘             └┘            └┘
par  ────────────┘        └┘             └┘            └┘
pid  ────────────┘        └┘             └┘            
st   ───────────────────────────────────────────────────┘└┘
569      intros m e, subst a', revert m, apply not_or_distrib.2,
id                         └┘                  └────────────┘
src      └────────┘  └────┘    └──────┘  └────┘└────────────┘└┘
typ      └────────┘  └────┘└┘  └──────┘  └────┘└────────────┘└┘
doc      └────────┘  └────┘    └──────┘  └────┘              └┘
txt      └────────┘  └────┘    └──────┘  └────┘              └┘
par      └────────┘  └────┘    └──────┘  └────┘              └┘
pid            └──┘                 └┘                     └┘
st   ─────────────┘└────────┘└────────┘└──────────────────────┘└─
570      have nd' := v.as_list_nodup _,
id                   └─────────────┘
src      └──────────┘└─────────────┘└┘
typ      └──────────┘└─────────────┘└┘
doc      └──────────┘               └┘
txt      └──────────┘               └┘
par      └──────────┘               └┘
pid      └──────┘└─┘               └┘
st   ────────────────────────────────┘└─
571      simp [hl, list.nodup_append] at nd', simp [nd'] },
id             └┘  └───────────────┘                └─┘
src      └────┘  └┘└───────────────┘└──────┘  └────┘   └┘
typ      └────┘└┘└┘└───────────────┘└──────┘  └────┘└─┘└┘
doc      └────┘  └┘                 └──────┘  └────┘   └┘
txt      └────┘  └┘                 └──────┘  └────┘   └┘
par      └────┘  └┘                 └──────┘  └────┘   └┘
pid            └┘                 └────┘         
st   ──────────────────────────────────────┘└───────────┘└┘
572    { suffices : ∀_:sigma.mk a' b' ∈ bucket_array.as_list bkts, a ≠ a',
id                                 └┘                        └──┘     └┘
src      
typ                               └┘                        └──┘     └┘
doc      
txt      
par      
pid      
st   ────┘
573      { simp [erase, @dif_neg (contains_aux a bkt) _ Hc, entries, and_iff_right_of_imp this] },
id                                             
typ                                            
st                                                                                              └┘
574      intros m e, subst a',
id                         └┘
typ                        └┘
575      exact Hc ((v.contains_aux_iff _ _).2 (list.mem_map_of_mem sigma.fst m)) }
st                                                                               └─
576  end
st   ──┘
577  
578  theorem find_erase_eq (m : hash_map α β) (a : α) : (m.erase a).find a = none :=
id                                                                   
typ                                                                  
579  begin
580    cases h : (m.erase a).find a with b, {refl},
st                                               └┘
581    exact absurd rfl ((mem_erase m a a b).1 ((find_iff (m.erase a) a b).1 h)).left
id                                                                     
typ                                                                    
582  end
st   └─┘
583  
584  theorem find_erase_ne (m : hash_map α β) (a a' : α) (h : a ≠ a') :
id                                                            └┘
typ                                                           └┘
585    (m.erase a).find a' = m.find a' :=
id                     └┘          └┘
typ                    └┘          └┘
586  option.eq_of_eq_some $ λb',
id                           └┘
typ                          └┘
587  (find_iff _ _ _).trans $ (mem_erase m a a' b').trans $
id                                          └┘ └┘
typ                                         └┘ └┘
588    (and_iff_right h).trans (find_iff _ _ _).symm
id                    
typ                   
589  
590  theorem find_erase (m : hash_map α β) (a' a : α) :
id                                               
typ                                              
591    (m.erase a).find a' = if a = a' then none else m.find a' :=
id                     └┘         └┘                       └┘
typ                    └┘         └┘                       └┘
592  if h : a = a' then by subst a'; simp [find_erase_eq m a]
id             └┘                                         
typ            └┘                                         
593  else by rw if_neg h; exact find_erase_ne m a a' h
id                                              └┘ 
typ                                             └┘ 
594  
595  section string
596  variables [has_to_string α] [∀ a, has_to_string (β a)]
id              └──┘  └──┘                     
src             └──┘  └──┘                  
typ             └──┘  └──┘                     
597  open prod
598  private def key_data_to_string (a : α) (b : β a) (first : bool) : string :=
id                                                          └──┘    └────┘
src                                                            └──┘    └────┘
typ                                                         └──┘    └────┘
599  (if first then "" else ", ") ++ sformat!"{a} ← {b}"
id       └┘ └┘
typ      └┘ └┘
600  
601  private def to_string (m : hash_map α β) : string :=
id                                            └────┘
src                                             └────┘
typ                                           └────┘
602  "⟨" ++ (fst (fold m ("", tt) (λ p a b, (fst p ++ key_data_to_string a b (snd p), ff)))) ++ "⟩"
id                            └┘                                               └┘
src                           └┘                                                      └┘
typ                           └┘                                               └┘
603  
604  instance : has_to_string (hash_map α β) :=
id                                       
typ                                      
605  ⟨to_string⟩
606  
607  end string
608  
609  section format
610  open format prod
611  variables [has_to_format α] [∀ a, has_to_format (β a)]
id                └──┘  └──┘                    
src               └──┘  └──┘                
typ               └──┘  └──┘                    
612  
613  private meta def format_key_data (a : α) (b : β a) (first : bool) : format :=
id                                                            └──┘    └──┘ 
src                                                              └──┘    └──┘ 
typ                                                           └──┘    └──┘ 
614  (if first then to_fmt "" else to_fmt "," ++ line) ++ to_fmt a ++ space ++ to_fmt "←" ++ space ++ to_fmt b
id       └───┘                                   └──┘                └───┘                  └───┘           
src                                              └──┘                 └───┘                  └───┘
typ      └───┘                                   └──┘                └───┘                  └───┘           
615  
616  private meta def to_format (m : hash_map α β) : format :=
id                                                 └────┘
src                                                  └────┘
typ                                                └────┘
617  group $ to_fmt "⟨" ++ nest 1 (fst (fold m (to_fmt "", tt) (λ p a b, (fst p ++ format_key_data a b (snd p), ff)))) ++
id    └┘                                                  └┘                                             └┘
src   └┘                                                  └┘                                                   └┘
typ   └┘                                                  └┘                                             └┘
618          to_fmt "⟩"
619  
620  meta instance : has_to_format (hash_map α β) :=
id                                            
typ                                           
621  ⟨to_format⟩
622  end format
623  end hash_map